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.1 of Proof General. See About for exact version. It is built for Emacs 23.2. The code *may* also work with Emacs 22.3, but you will need to regenerated the byte-compiled files with "make clean; make compile". Backward compatibility cannot be guaranteed. 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. /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 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 http://www.cs.kun.nl/~freek/comparison/. 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 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 January 2011.