1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
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 screen for exact version.
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>
September 2009.
|
