Deleted file

1 files changed, 0 insertions, 145 deletions

diff --git a/html/main.html b/html/main.html
deleted file mode 100644
index fdffc920..00000000
--- a/html/main.html
+++ /dev/null
@@ -1,145 +0,0 @@
-<h2>What is Proof General?</h2>
-<p>
-<b>Proof General</b> is a generic interface for proof assistants, 
-currently based on the customizable text editor <i>Emacs</i>.
-It works with either
-<a href="http://www.xemacs.org/">XEmacs</a> or
-<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
-Proof General 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>
-To find out more, check the
-<a href="features"> features list</a>
-and look at the
-<a href="screenshot">screenshots</a>.
-To get Proof General, visit the
-<a href="download">download page</a>.
-If you're not interested in interactive proof,
-see the <a href="components">standalone components</a>
-developed as part of Proof General.
-To contact the developers, click
-<?php hlink("feedback","here","Feedback form")?>.
-</p>
-
-
-
-<h2>What systems does Proof General work with?</h2>
-
-<p>Proof General comes ready-to-go for these proof
-assistants:</p>
-
-<table width="90%">
- <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">
-       By 
-      <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>
-       and
-       Markus Wenzel.
-       </div>
-   </td>
- </tr>
-  <tr>
-    <td align="center">
-       <?php hlink("http://pauillac.inria.fr/coq/",
-		   "<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/",
-		   "Coq","The Coq Home Page") ?>
-       <br>
-	<div style="font-size: smaller">
-         By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and
-	 <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
-        </div>
-    </td>
- </tr>
- <tr>
-    <td align="center">
-       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
-       "<img src=\"images/phox-einstein.jpg\" width=80 height=48 border=0 alt=\"PhoX logo\">",
-       "The PhoX Home Page") ?>
-   </td>
-    <td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for
-       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html",
-		   "PhoX","The PhoX Home Page") ?>
-       <br>
-       <div style="font-size: smaller">
-       By 
-       <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
-       and
-       <a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</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">
-       By Thomas Kleymann, Dilip Sequeira, 
-       <a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>
-       and
-       <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
-       </div>
-    </td>
- </tr>
-</table>
-
-<p>There are also <i>experimental</i> or <i>in-development</i> instances
-of Proof General:</p>
-
-<ul>
-<li><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>.</li>
-
-<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof
-General"); ?></b>, for <a
-href="http://www.twelf.org">Twelf</a>.</li>
-
-<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof
-General"); ?></b>, for <a
-href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.</li>
-
-<li><b><?php fileshow("ProofGeneral/plastic/README","Plastic Proof
-General"); ?></b>, for <a
-href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a> 
-(in development).</li>
-
-
-<li><b><?php fileshow("ProofGeneral/lclam/README","Lambda-Clam Proof
-General"); ?></b>, for <a href="http://dream.dai.ed.ac.uk/software/lambda-clam/">Lambda-CLAM</a>
-(in development).</li>
-</ul>
-
-<p>The instances of Proof General marked "in development" above are
-not considered complete, but are supported by the developers of proof
-systems.  The other instances above are "technology demonstrations" of
-Proof General for other popular provers, but only show a bare fraction
-of what is possible. We are seeking volunteers to support and improve
-each of these (please <a href="feedback">send a note to <tt><?php
-print $project_feedback; ?></tt></a> if you're interested).</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 <a
-href="ProofGeneral/doc/PG-adapting.pdf">documentation on
-configuration</a> is provided.</p>