Proof General --- Organize your proofs! 

Proof General is a generic Emacs interface for proof assistants.
The aim of the Proof General project is to provide a powerful, generic
environment for using interactive proof assistants.

This is version 4.0 of Proof General.  See About for exact version.

It is built for Emacs 23.  The code should also work with Emacs 22.3,
but you will need to regenerated the byte-compiled files with "make
clean; make compile".

See
    INSTALL	     for installation details.
    COPYING	     for license details.
    COMPATIBILITY    for version compatibility information.
    REGISTER	     for registration information (please register).
    FAQ, doc/	     for documentation of Proof General.
 
    <prover>/README  for additional prover-specific notes

Links:

    Bug/feature reports:  http://proofgeneral.inf.ed.ac.uk/trac 
    Wiki:		  http://proofgeneral.inf.ed.ac.uk/wiki
    Lists:		  http://proofgeneral.inf.ed.ac.uk/mailinglist

Supported proof assistants:  Coq, Isabelle, LEGO, PhoX, Plastic
Experimental (less useful):  CCC,ACL2,HOL98,Lambda-Clam,Shell,Twelf,Demoisa

A few example proofs are included in each prover subdirectory.  The
"root2" proofs of the irrationality of the square root of 2 were
proofs written for Freek Wiedijk's challenge in his comparison of
different theorem provers, see http://www.cs.kun.nl/~freek/comparison/.  
Those proof scripts are copyright by their named authors.  (NB: most
of these may have rusted)

Check BUGS files for some static problems and issues.  Please report
new bugs on the Trac site at http://proofgeneral.inf.ed.ac.uk/trac.

For the latest news and downloads, visit Proof General on the web 
at: http://proofgeneral.inf.ed.ac.uk

David Aspinall <da+pg-feedback@inf.ed.ac.uk>
August 2010.