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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
<h2>What is Proof General?</h2>
<p>
<b>Proof General</b> is a generic interface for proof assistants,
currently based on Emacs.
It has been developed at the
<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>
in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>.
</p>
<p>
Proof General
works best under
<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with
<a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
You need a recent version in either case.
</p>
<p>
The aim of the Proof General project is to provide a powerful and
configurable interfaces which help user-interaction with interactive
proof assistants. The strategy of Proof General is to target power
users rather than novices, but we include general user interface
niceties, such as toolbar and menus, which make use easier for all.
<p>
To read more about what Proof General
provides,
<?php link_root("features","check the features list") ?>.
To see what Proof General looks like in use, have a look at these
<a href="screenshot.phtml">screenshots</a>.
To download Proof General, visit the
<?php link_root("download","download page") ?>.
To contact the developers, click
<?php hlink("feedback.phtml","here","Feedback form")?>.
</p>
<h2>What systems does Proof General work with?</h2>
<p>
Proof General comes ready-customized for several proof assistants,
including:
</p>
<table width="90%">
<tr>
<td align="center">
<?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
"<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?>
</td>
<td>
<b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for
<?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
"Coq","The Coq Home Page") ?>
<br>
<div style="font-size: smaller">
First crafted by
<a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>.
<br>
Contributions by Patrick Loiseleur.
<br>
Maintained by
<a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
"The Isabelle Home Page"); ?>
</td>
<td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"Isabelle", "The Isabelle Home Page"); ?>
<br>
<div style="font-size: smaller">
Crafted and maintained by
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
<br>
Additional maintainance, support for
<a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
by
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
"The LEGO Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"LEGO","The LEGO Home Page") ?>
<br>
<div style="font-size: smaller">
First crafted by <a href="http://www.dcs.ed.ac.uk/~tms">Thomas Kleymann</a>
and
<a href="http://www.dcs.ed.ac.uk/~djs/welcome.html">Dilip Sequeira</a>.
<br>
Maintained by
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
and
<a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
"AF2",
"The AF2 Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/AF2/README","AF2 Proof General "); ?></b> for
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
"AF2","The AF2 Home Page") ?>
<br>
<div style="font-size: smaller">
Crafted and maintained by
<a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
</div>
</td>
</tr>
</table>
<p>
There is also a preliminary version of
<b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>, for
<a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.
We are seeking a volunteer from the HOL community to support
and improve this (perhaps also supporting other HOL variants).
</p>
<p>
Proof General is ready to be customized to new proof assistants.
It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
"very easy"); ?> to get basic support working.
Full documentation on configuration is provided.
</p>
|
