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.

Proof General is ready-customized for several proof assistants:

","The Coq Home Page") ?> Coq Proof General for version 6.2

First crafted by Healfdene Goguen.
Currently maintained and developed by Patrick Loiseleur.

", "The LEGO Home Page") ?> LEGO Proof General version 1.3.1

First crafted by Thomas Kleymann and Dilip Sequeira.
Maintained by Paul Callaghan.

", "The Isabelle Home Page"); ?> Isabelle Proof General for version 99

Crafted and maintained by David Aspinall.
Support for Isabelle/Isar is provided by Markus Wenzel.

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

You can download Proof General or contact the developers .

","The Coq Home Page") ?>	Coq Proof General for version 6.2 First crafted by Healfdene Goguen. Currently maintained and developed by Patrick Loiseleur.
", "The LEGO Home Page") ?>	LEGO Proof General version 1.3.1 First crafted by Thomas Kleymann and Dilip Sequeira. Maintained by Paul Callaghan.
", "The Isabelle Home Page"); ?>	Isabelle Proof General for version 99 Crafted and maintained by David Aspinall. Support for Isabelle/Isar is provided by Markus Wenzel.