New web pages

1 files changed, 63 insertions, 0 deletions

diff --git a/html/doc.phtml b/html/doc.phtml
new file mode 100644
index 00000000..5f90f3f9
--- /dev/null
+++ b/html/doc.phtml
@@ -0,0 +1,63 @@
+<h2>Manual</h3>
+
+<p>
+Full documentation for Proof General 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>
+For convenience, the documentation is also available in HTML 
+<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","here.","","html") ?>
+<br>
+You can download the 
+<a href="ProofGeneral/doc/ProofGeneral.dvi">dvi</a>,
+<a href="ProofGeneral/doc/ProofGeneral.ps">ps</a>,
+or
+<a href="ProofGeneral/doc/ProofGeneral.pdf">pdf</a> 
+versions for printing.
+</p>
+
+<p>
+<it>Note:</it> the documentation above is taken from the current
+pre-release and may be updated from the documentation included
+in the last stable release.
+</p>
+
+<hr>
+<h2>References</h2>
+
+<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>
+