From bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 15:01:50 +0000
Subject: Renamed file

---
 html/main.phtml | 138 --------------------------------------------------------
 1 file changed, 138 deletions(-)
 delete mode 100644 html/main.phtml

(limited to 'html/main.phtml')

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>
-
-
-- 
cgit v1.2.3