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. Currently maintained and developed by Patrick Loiseleur.
", "The LEGO Home Page") ?>	LEGO Proof General for First crafted by Thomas Kleymann and Dilip Sequeira. Maintained by Paul Callaghan.
", "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.

To see what Proof General looks like in use, have a look at this screenshot.

You can download Proof General or contact the developers .