Proof General is a generic interface for proof assistants, currently based on Emacs. It has been developed at the LFCS in the University of Edinburgh.
Proof General works best under XEmacs, but can also be used with FSF GNU Emacs. You need a recent version in either case.
To read more about what Proof General provides, . To see what Proof General looks like in use, have a look at these screenshots. To download Proof General, visit the . To contact the developers, click .
Proof General comes ready-customized for several proof assistants, including:
| ","The Coq Home Page") ?> |
for
|
| ", "The LEGO Home Page") ?> | for
First crafted by Thomas Kleymann
and
Dilip Sequeira.
Maintained by David Aspinall and Paul Callaghan. |
| ", "The Isabelle Home Page"); ?> | for
|
There is also a preliminary version of , for HOL98. We are seeking a volunteer from the HOL community to support and improve this (perhaps also supporting other HOL variants).
Proof General is ready to be customized to new proof assistants. It can be to get basic support working. Full documentation on configuration is provided.