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.
It is supplied ready-customized for several proof assistants:

Coq Proof General for version 6.2

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

LEGO Proof General version 1.3.1

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

Isabelle Proof General for version 98-1

Crafted and maintained by David Aspinall.

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

You can download Proof General or contact the developers .

	Coq Proof General for version 6.2 First crafted by Healfdene Goguen. Currently maintained and developed by Patrick Loiseleur.
	LEGO Proof General version 1.3.1 First crafted by Thomas Kleymann and Dilip Sequeira. Maintained by Paul Callaghan.
	Isabelle Proof General for version 98-1 Crafted and maintained by David Aspinall.