blob: 857a7ad17ecb945c7d752f0a1c4bfb3abaca715f (
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
|
<!-- <h2><a name="about">About Proof General</a></h2> -->
<h2>The Proof General project</h2>
<p>
The forefather of Proof General was LEGO mode, begun by Thomas
Kleymann in 1994 as an Emacs-based front end for LEGO similar to <a
href="http://www.dcs.ed.ac.uk/home/da/Isamode">Isamode</a>. Later,
implementations of proof-by-pointing and script management were added,
and the code was made generic.
</p>
<p>
This generic basis for Proof General was further developed at the
<a href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a> by Kleymann, Sequeira,
Goguen and Aspinall (in order of appearance).
It follows some of the ideas used in
<a href="http://www.inria.fr/croap/">Project CROAP</a>.
The authors and current 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 <a
href="http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html">EPSRC</a>
and the <a
href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>.
</p>
<p>
For more on the history of the development of
Proof General, 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>
|
