blob: 642beba93a9ce8e8aa33bfeef3a8578d5dfc1c8a (
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
|
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.
|
