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

To read more about what features Proof General provides, .
To see what Proof General looks like in use, have a look at these screenshots.

Proof General is ready-customized for several proof assistants, including:

","The Coq Home Page") ?>	for First crafted by Healfdene Goguen. Maintained by Pierre Courtieu.
", "The LEGO Home Page") ?>	for First crafted by Thomas Kleymann and Dilip Sequeira. Maintained by David Aspinall and Paul Callaghan.
", "The Isabelle Home Page"); ?>	for Crafted and maintained by David Aspinall. Additional maintainance, support for by Markus Wenzel.

There is also a preliminary version of , for HOL98. We are seeking a volunteer from the HOL community to support and improve this (perhaps also supporting other HOL variants).

Proof General is ready to be customized to new proof assistants.
It can be to get basic support working.
Full documentation on configuration is provided.

You can download Proof General or contact the developers .