aboutsummaryrefslogtreecommitdiff
path: root/html/main.phtml
diff options
context:
space:
mode:
authorDavid Aspinall2000-09-28 15:01:50 +0000
committerDavid Aspinall2000-09-28 15:01:50 +0000
commitbd7aa7923a25d16207842f9f3d6b773c2fc6fa58 (patch)
tree8f5733bf63e8c880e65472b3ebf745b1026698e3 /html/main.phtml
parent2c253444d0b93cf7628ab030e6a5f1ad24fa20fd (diff)
Renamed file
Diffstat (limited to 'html/main.phtml')
-rw-r--r--html/main.phtml138
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>
-
-