Title: Proof General: A Generic Tool for Proof Development
Abstract: This note describes Proof General, a tool for developing machine proofs with an interactive proof assistant. Interaction is based around a proof script, which is the target of a proof development. Proof General provides a powerful user-interface with relatively little effort, alleviating the need for a proof assistant to provide its own GUI, and providing a uniform appearance for diverse proof assistants. Proof General has a growing user base and is currently used for several interactive proof systems, including Coq, LEGO, and Isabelle. Support for others is on the way. Here we give a brief overview of what Proof General does and the philosophy behind it; technical details are available elsewhere. The program and user documentation are available on the web at http://www.dcs.ed.ac.uk/home/proofgen .