It doesn't matter if you're an Emacs militant or a pacifist!
Proof General will be useful to you if you use a proof assistant, and you'd like some of the following features:
Proof General colours a proof script to show the state in the proof assistant. Parts of a proof script that have been processed are displayed in blue and are "locked" -- they cannot be edited. Parts of the script currently being processed by the proof assistant are shown in red. Commands are provided to process new parts of the buffer, or undo already processed parts.
Take a look at this screenshot of Proof General to see script managament in action.
Dependencies between script files are communicated from the proof assistant to Proof General. If you want to edit a file which has been loaded into the proof assistant already, Proof General will unlock the file and all the files which depend on it. This connects the editor with the theory dependency or make system of the proof assistant.
Proof by pointing uses the interface to highlight subterms under the mouse, and Proof General uses the subterm structure to make it easy to cut and paste complicated subterms.
Using the toolbar, you can replay proofs without knowing any low-level commands of the proof assistant or any Emacs hot-keys!
Proof General decorates proof scripts: proof commands are highlighted and different fonts may be used for definitions and assumptions, for example.
Proof General is supplied with utilities to make tag indexes for Emacs. This makes it easy to quickly access definitions from a standard library, for example, and in large proof developments split across multiple files.
Adapting for a new proof assistant is mainly a matter of setting some variables with regular expressions to help parse output from the prover, and setting other variables with commands to send to the prover. To get the most from Proof General (proof-by-pointing, for example), it may be necessary to augment the output routines of the proof assistant.
Please feel free to download Proof General to customize it for a new system, and how you get on.For more details of the above features, see the