blob: b9ee6c058fd9f8568f2a8f079504aa9ef7bc8666 (
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
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
|
<!-- <?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.
</p>
<p>
It
works best under
<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with
<a href="ftp://prep.ai.mit.edu/pub/gnu/emacs/">FSF GNU Emacs</a>.
<br>
It is supplied ready-customized for several proof assistants:
</p>
<p>
<table width=90%>
<tr>
<td align="centre">
<img src="images/coq-badge.gif" width="110" height="35" alt="Coq badge"></td>
<td>
<b> Coq Proof General </b> for
<?php hlink("http://pauillac.inria.fr/coq/assis-eng.html",
"Coq","The Coq Home Page") ?>
version 6.2
<br>
<div style="font-size: smaller">
First crafted by
<a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>.
<br>
Currently maintained and developed by Patrick Loiseleur.
</div>
</td>
</tr>
<tr>
<td align="centre">
<img src="images/lego-badge.gif" width="123" height="33" alt="LEGO badge"></td>
<td><b>LEGO Proof General</b>
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"LEGO","The LEGO Home Page") ?>
version 1.3.1
<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="centre">
<img src="images/isabelle-badge.gif" width="128" height="37"
alt="Isabelle badge"></td>
<td><b> Isabelle Proof General </b> for
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"Isabelle", "The Isabelle Home Page"); ?>
version 98-1
<br>
<div style="font-size: smaller">
Crafted and maintained by
<a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
</div>
</td>
</tr>
</table>
</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>
|
