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:

Coq badge Coq Proof General for version 6.2
First crafted by Healfdene Goguen.
Currently maintained and developed by Patrick Loiseleur.
LEGO badge LEGO Proof General version 1.3.1
First crafted by Thomas Kleymann and Dilip Sequeira.
Maintained by Paul Callaghan.
Isabelle badge 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 .