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 20.X (or later) version in either case.
For detailed version numbers, check the
Proof General is ready-customized for several proof assistants, including:
","The Coq Home Page") ?> |
Coq Proof General for
|
", "The LEGO Home Page") ?> | LEGO Proof General for
|
", "The Isabelle Home Page"); ?> | Isabelle Proof General for
Crafted and maintained by
David Aspinall.
Additional maintainance and support for Isabelle/Isar is provided by Markus Wenzel. |
We also supply instructions for how to customize Proof General to new
proof assistants.
Experimental support for new proof assistants is
made available in our developers release.
To see what Proof General looks like in use, have a look at this screenshot.
You can download Proof General or contact the developers .