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
|
<h2>About the Proof General project</h2>
<p>
The forefather of Proof General was LEGO mode, begun in 1994 at the <a
href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a> by Thomas Kleymann. LEGO
mode was an Emacs-based front end for LEGO similar to David Aspinall's
<a href="http://zermelo.dcs.ed.ac.uk/~isamode">Isamode</a>,
developed at the LFCS since 1992. After 1994, implementations of
proof-by-pointing and script management were added to LEGO mode, and
the code was made generic. The generic basis was developed by
Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall.
The current authors and maintainers of the various instantiations of
Proof General are mentioned on the <?php link_root("main","front
page.") ?>
</p>
<p>
The Proof General project was coordinated until October 1998 by
Thomas Kleymann, and since then by David Aspinall. The project has
benefited from funding by
<!-- this link is broken: <a href="http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html"> -->
EPSRC,
<!-- (Applications of a Type Theory based Proof Assistant) -->
<!-- </a>, -->
the <a
href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>,
and the <a href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a>.
</p>
<p>
David Aspinall designed the web pages and graphics for Proof General.
<br>
Check the <a href="gallery.phtml">gallery</a> for more publicity
pictures!
</p>
<p>
For more on the history of the development of
the Proof General program, see the
<?php htmlshow("ProofGeneral/doc/ProofGeneral_1.html#SEC3","manual preface.","","html") ?>
</p>
<h2>Contact information</h2>
<p>
Have you any questions, comments, or suggestions about Proof General?
<br>
Send us a message using <a href="feedback.phtml">this form</a>.
</p>
<p>
Discuss Proof General with other users and receive
announcements by joining our <a href="mailinglist.phtml">mailing
list</a>.
</p>
|
