Author: Lucas Dixon
Title: IsaPlanner: A proof planning framework for Isabelle
Abstract: 
We introduce our work on the development of a proof planner for Isabelle and 
highlight some recent developments. The central aim of this work is to improve 
automation in Isabelle by employing techniques, such as rippling, from the 
paradigm of proof planning. A second goal of our work is to use the 
correspondence between proof plans and Isar proof scripts to provide tools for 
the automatic generation and manipulation of proof scripts.