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
|
<!-- <?php print $separator; ?> -->
<!-- <a href="#what">What</a> -->
<!-- <?php print $separator; ?> -->
<!-- <a href="#why">Why</a> -->
<!-- <?php print $separator; ?> -->
<!-- <a href="#about">About</a> -->
<!-- </br> -->
<!-- <h2><a name="what">What is Proof General?</a></h2> -->
<p>
<b>Proof General</b> is a generic interface for proof assistants,
based on Emacs.<br>
It has been developed at the
<a href="http://www.dcs.ed.ac.uk/lfcs">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>.
<br>
You need a 20.X (or later) version in either case.
For detailed version numbers, check the
<?php link_root("download","download page.") ?>
</p>
<p>
Proof General is 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> 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>
<b>No current maintainer.
<a href="feedback.phtml">Please offer to help!!</a>.
</b>
</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>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">Dilip Sequeira</a>.
<br>
Maintained by <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> 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 and support for
<a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar</a>
is provided by
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
</div>
</td>
</tr>
</table>
<p>
We also supply instructions for how to customize Proof General to new
proof assistants.
</p>
<p>
To see what Proof General looks like in use, have a look at this
<a href="screenshot.phtml">screenshot</a>.
</p>
<p>
You can download Proof General
<?php link_root("download","here") ?> or contact the developers
<?php hlink("feedback.phtml","here","Feedback form")?>.
</p>
|
