Proof General is a generic interface for proof assistants, currently
based on the customizable text editor Emacs. It works with either
XEmacs or GNU Emacs. A new Eclipse-based version is in development.
This is described separately at http://proofgeneral.inf.ed.ac.uk/kit/wiki.

Proof General has been developed at the LFCS in the University of
Edinburgh. It is distributed under the conditions of the GNU General
Public License.

There is a mailing list:
	http://proofgeneral.inf.ed.ac.uk/mailinglist

WWW: http://proofgeneral.inf.ed.ac.uk