aboutsummaryrefslogtreecommitdiff
path: root/html
diff options
context:
space:
mode:
authorDavid Aspinall1999-06-28 16:03:59 +0000
committerDavid Aspinall1999-06-28 16:03:59 +0000
commit900e3f8add7218d97965d6802fe8b88f81a91625 (patch)
treeb2ad35dfbea9c7fb7bdd69717bc0c2a211733fc6 /html
parent4d1262eee90bb4ae0cb32bcc08b9c8223ef3ac3f (diff)
Paraphrased some of the history.
Diffstat (limited to 'html')
-rw-r--r--html/about.phtml30
1 files changed, 18 insertions, 12 deletions
diff --git a/html/about.phtml b/html/about.phtml
index 7db1f29e..6a317558 100644
--- a/html/about.phtml
+++ b/html/about.phtml
@@ -1,35 +1,41 @@
<!-- <h2><a name="about">About Proof General</a></h2> -->
<h2>The Proof General project</h2>
<p>
-The Proof General project was initiated in 1994 (under the name of
-"lego-mode") and coordinated until October 1998 by Thomas
-Kleymann. Since October 1998, David Aspinall has been in charge of
-Proof General.
-<p>
-<p>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>.
+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>
-The generic base for Proof General was developed at the
+This generic base for Proof General was 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>.
-</p>
-<p>
+
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>