Proof General

Proof General is a proof assistant interface that is implemented in Emacs Lisp,and supports a variety of proof assistants. Four proof assistants have strong support- Isabelle, Coq, PhoX and LEGO, with experimental support for HOL, Twelf [45], ACL2 [27], Plastic [15] and Lambda-CLAM. This flexibility has made Proof General perhaps the most successful theorem prover interface, being widely used and has become the de facto standard interface for Isabelle. Like Pcoq it allows the use of proof by pointing, and is based around a similar three-paned layout.

A few drawbacks of Proof General's design are pointed out by Aspinall in his descriptions [6] of the works in progress planned for future releases. The primary concern is the reliance on Emacs, which is enough to dissuade many people who don't use, or don't like Emacs. Next is that there is not enough customisation to the particular proof engine being used (the generality of Proof General has come back to bite the developers and ultimately users), there is a desire that the proof interface should require the user to know as little as possible of the underlying proof assistant syntax. To proof-assistant-specific commands, such as applying tactics to a proof in Isabelle, the user needs to enter a command line in Isabelle's internal syntax.

A number of other graphical user interfaces to the target proof engine (Isabelle) in this project exist, brief descriptions of the most interesting of these are described below.