Proof General is a generic interface for proof assistants,
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.
For detailed version numbers, check the
To read more about what features Proof General
provides,
.
To see what Proof General looks like in use, have a look at these
screenshots.
Proof General is 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.
You can download Proof General or contact the developers .