Renamed file

1 files changed, 0 insertions, 88 deletions

diff --git a/html/doc.phtml b/html/doc.phtml
deleted file mode 100644
index e8ae6b98..00000000
--- a/html/doc.phtml
+++ /dev/null
@@ -1,88 +0,0 @@
-<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>
-