Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Proof General theorem prover interface --- IN ATTIC BECAUSE: last cvs standing, see
Emacs Lisp OCaml Coq XSLT TeX Shell Other
Branch: master
Failed to load latest commit information.
acl2 Clean whitespace
bin Quote arguments to EMACS/PGHOME.
ccc Cleanup
contrib remove backup file
coq Fixing coq project file parsing + moved project options.
doc Added some information on coq project file in doc.
etc Set version tag for new release.
generic Set version tag for new release.
hol-light - support bullets and braces in Prooftree
hol98 Replace proof-terminal-char with proof-terminal-string.
html Deleted file
images rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif}
isar unicode tokens for \<open>, \<close>, \<newline>;
lego Summary: Don't quote lambda expressions
lib Added comment.
obsolete Summary: Don't quote lambda expressions
pghaskell Fix name in proof-easy-config, addressing Trac #441
pgocaml New pseudo instances to help tool demonstrators in ocaml/ghci (in pro…
pgshell Replace proof-terminal-char with proof-terminal-string.
phox Summary: Don't quote lambda expressions
twelf Clean whitespace
.cvsignore Updated.
AUTHORS Add note about short list
BUGS Emphasise importance of Trac
CHANGES Fixing undeclared variables for compilation.
COMPATIBILITY Drop support for Emacs 23.1 and earlier
FAQ Change default Unicode Tokens font back to DejaVU Sans, more reliable…
Makefile Document Make check
Makefile.devel Remove link in tar file.
README Bump doc version numbers to 4.2pre.
REGISTER Fix domain name
TAGS update TAGS


	    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.2 (prerelease) of Proof General.  See About for exact version.
It is built for Emacs 23.3.

The code *may* also work with previous emacs versions, back as far as
Emacs 22.3.  But you will need to regenerated the byte-compiled files
with "make clean; make compile".  Backward compatibility cannot be

    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


    Bug/feature reports: 

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

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  
Those proof scripts are copyright by their named authors.  
(NB: most of these have rusted)

Check BUGS files for some static problems and issues.  Please report
new bugs on the Trac site at

For the latest news and downloads, visit Proof General on the web 

David Aspinall <>
October 2011.
Something went wrong with that request. Please try again.