Higher Order Rippling in IsaPlanner

L. Dixon, J. D. Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present an account of rippling with proof critics suitable for use in higher order logic in Isabelle/IsaPlanner. We treat issues not previously examined, in particular regarding the existence of multiple annotations during rippling. This results in an efficient mechanism for rippling that can conjecture and prove needed lemmas automatically as well as present the resulting proof plans as Isar style proof scripts.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-30142-4
ISBN (Print)978-3-540-23017-5
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Cite this