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 GNU Emacs. You need a recent version in either case.
To read more about what Proof General is and what it provides, check the features list. To see what Proof General looks like in use, have a look at these screenshots. To download Proof General, visit the download page. To contact the developers, click .
Proof General comes ready-customized for these proof assistants:
| ", "The Isabelle Home Page"); ?> | for
By
David Aspinall
and
Markus Wenzel.
|
| ","The Coq Home Page") ?> |
for
By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
Pierre Courtieu.
|
| ", "The PhoX Home Page") ?> | for
By
Christophe Raffalli
and
Paul Roziere.
|
| ", "The LEGO Home Page") ?> | for
By Thomas Kleymann, Dilip Sequeira,
David Aspinall
and
Paul Callaghan.
|
There are also experimental instances of Proof General:
These instances of Proof General are functional, but only show a bare fraction of what is possible. We are seeking volunteers to support and improve each of these (please send a note to if you're interested).
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.