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
|
<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>
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>
</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/coq-badge.gif\" width=110 height=35 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>
Maintained by
<a href="mailto:courtieu@lri.fr">Pierre Courtieu</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://www.dcs.ed.ac.uk/~da">David Aspinall</a>
and
<a href="http://www.dur.ac.uk/~dcs1pcc/">Paul Callaghan</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"<img src=\"images/isabelle-badge.gif\" width=128 height=37 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://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
<br>
Additional maintainance, support for
<?php fileshow("ProofGeneral/isar/README","Isabelle/Isar "); ?>
by
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</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>
|
