diff options
| author | David Aspinall | 2000-09-28 15:01:50 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-09-28 15:01:50 +0000 |
| commit | bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 (patch) | |
| tree | 8f5733bf63e8c880e65472b3ebf745b1026698e3 /html/main.phtml | |
| parent | 2c253444d0b93cf7628ab030e6a5f1ad24fa20fd (diff) | |
Renamed file
Diffstat (limited to 'html/main.phtml')
| -rw-r--r-- | html/main.phtml | 138 |
1 files changed, 0 insertions, 138 deletions
diff --git a/html/main.phtml b/html/main.phtml deleted file mode 100644 index 7844d527..00000000 --- a/html/main.phtml +++ /dev/null @@ -1,138 +0,0 @@ -<h2>What is Proof General?</h2> -<p> -<b>Proof General</b> is a generic interface for proof assistants, -currently based on Emacs. -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>. -You need a recent version in either case. -</p> -<p> -The aim of the Proof General project is to provide a powerful and -configurable interfaces which help user-interaction with interactive -proof assistants. The strategy of Proof General is to target power -users rather than novices, but we include general user interface -niceties, such as toolbar and menus, which make use easier for all. -<p> -To read more about what Proof General -provides, -<?php link_root("features","check the features list") ?>. -To see what Proof General looks like in use, have a look at these -<a href="screenshot.phtml">screenshots</a>. -To download Proof General, visit the -<?php link_root("download","download page") ?>. -To contact the developers, click -<?php hlink("feedback.phtml","here","Feedback form")?>. -</p> - - - -<h2>What systems does Proof General work with?</h2> -<p> -Proof General comes 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/coqlogo4.gif\" width=66 height=61 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> - Contributions by Patrick Loiseleur. - <br> - Maintained by - <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>. - </div> - </td> - </tr> - <tr> - <td align="center"> - <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/", - "<img src=\"images/isabelle.gif\" width=74 height=64 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://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>. - <br> - Additional maintainance, support for - <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a> - by - <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</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://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a> - and - <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>. - </div> - </td> - </tr> - <tr> - <td align="center"> - <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html", - "AF2", - "The AF2 Home Page") ?> - </td> - <td><b><?php fileshow("ProofGeneral/AF2/README","AF2 Proof General "); ?></b> for - <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html", - "AF2","The AF2 Home Page") ?> - <br> - <div style="font-size: smaller"> - Crafted and maintained by - <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</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. -It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", -"very easy"); ?> to get basic support working. -Full documentation on configuration is provided. -</p> - - |
