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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
Proof General --- Organize your proofs! [proofgeneral.inf.ed.ac.uk]
=========================================================================
| |
| IMPORTANT NOTE: Please note that proofgeneral.org is no longer owned |
| by the Proof General project; please update your links to use the |
| new web address http://proofgeneral.inf.ed.ac.uk. |
| |
| Report bugs, feedback, suggestions directly to me. It helps if you |
| use one of the suggested + extensions to my mail address, e.g. |
| |
| David Aspinall <da+pg-feedback@inf.ed.ac.uk> |
| |
=========================================================================
Proof General is a generic Emacs interface for proof assistants.
This is version 3.6 of Proof General.
(Check About screen for a precise version number; also see CHANGES).
The aim of the Proof General project is to provide a powerful and
configurable interfaces which help user-interaction with interactive
proof assistants. Proof General targets power users rather than
novices, but we include general user interface niceties, such as
toolbar and menus, which make use easier for all.
Please help us with this aim! Configure Proof General for your proof
assistant, by adding features at the generic level wherever possible.
Send ideas, comments, patches, code to da+pg-feedback@inf.ed.ac.uk
See INSTALL for installation details.
COPYING for license details.
REGISTER for registration information (please register).
FAQ, doc/ for documentation of Proof General.
See http://proofgeneral.inf.ed.ac.uk/mailinglist for the Proof General
mailing lists. If you have problems, please contact
da+pg-support@inf.ed.ac.uk after checking the BUGS and CHANGES files.
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, in this directory, and for
specific issues, in each prover subdirectory. Please report bugs
not mentioned in any of these files to da+pg-bugs@inf.ed.ac.uk
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 2004.
|