aboutsummaryrefslogtreecommitdiffhomepage
path: root/html/main.phtml
blob: 30dc84a17d08b429301edd6fe2168241ef4f9647 (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
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
<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.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>.
<br>
You need a recent version in either case.
For detailed version numbers, check the
<?php link_root("download","download page.") ?> 
</p>

<p>
To read more about what features Proof General
provides, 
<?php link_root("features","click here") ?>.
<br>
To see what Proof General looks like in use, have a look at these
<a href="screenshot.phtml">screenshots</a>.
</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><?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.
<br>
It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
"very easy"); ?> to get basic support working.
<br>
Full documentation on configuration is provided.
</p>


<p>
You can download Proof General 
<?php link_root("download","here") ?> or contact the developers 
<?php hlink("feedback.phtml","here","Feedback form")?>.
</p>