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

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. Experimental support for new proof assistants is made available in our developers release.

To read more about what features Proof General provides, .
To see what Proof General looks like in use, have a look at these screenshots.

You can download Proof General or contact the developers .