Renamed file

1 files changed, 138 insertions, 0 deletions

diff --git a/html/main.html b/html/main.html
new file mode 100644
index 00000000..7844d527
--- /dev/null
+++ b/html/main.html
@@ -0,0 +1,138 @@
+<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>
+
+