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 Coq Home Page") ?> |
for
First crafted by
Healfdene Goguen.
Contributions by Patrick Loiseleur. Maintained by Pierre Courtieu. |
| ", "The Isabelle Home Page"); ?> | for
Crafted and maintained by
David Aspinall.
Additional maintainance, support for Isabelle/Isar by Markus Wenzel. |
| ", "The LEGO Home Page") ?> | for
First crafted by Thomas Kleymann
and
Dilip Sequeira.
Maintained by David Aspinall and Paul Callaghan. |
| for
Crafted and maintained by
Christophe Raffalli
and
Paul Roziere.
|
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.