Wikipedia
IsaPlanner
IsaPlanner is a proof planner for the interactive proof assistant, Isabelle. Originally developed by Lucas Dixon as part of his PhD thesis at the University of Edinburgh, it is now maintained by members of the Mathematical Reasoning Group, in the School of Informatics at Edinburgh. IsaPlanner is the latest of a series of proof planners written at Edinburgh. Earlier planners include Clam and LambdaClam.