blob: 2da03478e4f5fbd8742094c3d848522a5fdc0740 (
plain)
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
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 3.7.1 of Proof General.
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.
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.
(NB: some of these may have rusted)
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>
January 2008.
|
