Renamed file

1 files changed, 88 insertions, 0 deletions

diff --git a/html/doc.html b/html/doc.html
new file mode 100644
index 00000000..e8ae6b98
--- /dev/null
+++ b/html/doc.html
@@ -0,0 +1,88 @@
+<h2>Manual</h2>
+
+<p>
+Here is the  
+<?php htmlshow("ProofGeneral-3.1/doc/ProofGeneral_toc.html","Proof General user manual","Proof General Manual") ?> in HTML form, as included in the distribution.
+<br>
+For printing you can download the 
+<?php download_link("ProofGeneral-3.1/doc/ProofGeneral.ps.gz", "gzipped ps file") ?> 
+(recommended) or the 
+<?php download_link("ProofGeneral-3.1/doc/ProofGeneral.pdf", "pdf file") ?>.
+</p>
+
+<p>
+The manual (in HTML and Info formats), as well as other documentation,
+is included in the <?php link_root("download","download.") ?> When
+running Proof General the manual is available from the "Proof General"
+menu.  It should also appear in the system Info pages.
+</p>
+
+
+<p>
+You can discuss Proof General with other users and receive
+announcements by joining our <a href="mailinglist.phtml">mailing
+list</a>.
+</p>
+
+<h2>References</h2>
+
+<p> Ideas for the future of Proof General are given here:
+</p>
+<ul>
+<li><a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+    <b><i>Protocols for Interactive e-Proof</i></b>.
+    Draft version, see 
+    <a href="http://zermelo.dcs.ed.ac.uk/~da/drafts/#eproof">here</a>.
+</li>
+<li><a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
+    <b><i>Proof General Kit (white paper)</i></b>.
+    Draft version, see 
+    <a href="http://zermelo.dcs.ed.ac.uk/home/da/drafts/#white">here</a>.
+</li>
+</ul>
+<p> A technology overview of Proof General is given here:
+</p>
+<ul>
+<li> <a href="http://www.dcs.ed.ac.uk/home/da">David Aspinall</a>.
+    <a href="papers/pgoutline.ps.gz">Proof General: A Generic Tool for
+     Proof Development</a>.
+     <i>Tools and Algorithms for the Construction and 
+      Analysis of Systems, Proc TACAS 2000</i>, LNCS 1785.
+    <br>
+    Here are some <a href="papers/pgtalk.pdf">slides</a> 
+    used for this talk and some other presentations of Proof General.
+</li>
+</ul>
+<p> Proof General supports Script Management as documented in:
+</p>
+<ul>
+  <li> <a
+      href="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
+      Bertot</a> and <a
+      href="http://www.inria.fr/croap/personnel/Laurent.Thery/me.html">Laurent
+      Th&eacute;ry</a>.  <a
+      href="ftp://babar.inria.fr/pub/croap/bertot/jsymcomp.ps">A
+      generic approach to building user interfaces for theorem
+      provers</a>.  
+      <i>Journal of Symbolic Computation</i>, 25(7), pp. 161-194, February 1998.
+  </li>
+ </ul>
+ <p>
+ It has support for Proof by Pointing, as documented in:
+ </p>
+ <ul>
+  <li> <A
+      HREF="http://www.inria.fr/croap/personnel/Yves.Bertot/me.html">Yves
+      Bertot</A>, <A HREF="http://www.dcs.ed.ac.uk/home/tms">
+      Thomas Kleymann-Schreiber</A> and <A
+      HREF="http://www.dcs.ed.ac.uk/home/djs">Dilip Sequeira</a>.
+    <I>Implementing Proof by Pointing without a Structure Editor</I>.
+    LFCS Technical Report <A
+    HREF="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/97/ECS-LFCS-97-368/index.html">ECS-LFCS-97-368</a>.
+    Also published as Rapport de recherche de l'INRIA
+    <A HREF="http://www.inria.fr/Unites/SOPHIA-eng.html"> Sophia
+      Antipolis</a> <A
+      HREF="http://www.inria.fr/RRRT/RR-3286.html">RR-3286</a>
+  </li>
+</ul>
+