Proof General --- Organize your proofs! 

Proof General is a generic Emacs interface for proof assistants.

This is version 3.7 of Proof General (see about screen for exact version).   

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

See

    INSTALL   for installation details.
    COPYING   for license details.
    REGISTER  for registration information (please register).
    FAQ, doc/ for documentation of Proof General.

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


For notes on the supported assistants, see the README files
in the subdirectories:

    acl2/   ACL2
    phox/   PhoX
     coq/   Coq
 demoisa/   Demonstration instance for Isabelle
   hol98/   HOL 98
     isa/   Isabelle
    isar/   Isabelle/Isar
    lego/   LEGO
 plastic/   Plastic
   twelf/   Twelf
   pgkit/   PG Kit

 generic/   Generic basis for Proof General

A small number of example proofs are included in each prover 
subdirectory.   The "root2" example proofs of the irrationality
of the square root of 2 were proofs written as a response
to a challenge of Freek Wiedijk in his comparison of different
theorem provers, see http://www.cs.kun.nl/~freek/comparison/.
Those proof scripts are copyright by their named authors.

Check BUGS files for 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>
June 2007.