Proof General is a generic interface for proof assistants, based on Emacs.

It 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.