diff options
Diffstat (limited to 'html/doc.html')
| -rw-r--r-- | html/doc.html | 140 |
1 files changed, 0 insertions, 140 deletions
diff --git a/html/doc.html b/html/doc.html deleted file mode 100644 index 466add09..00000000 --- a/html/doc.html +++ /dev/null @@ -1,140 +0,0 @@ -<h2>Manuals for Proof General</h2> - -<p> -There is a short FAQ and two manuals for Proof General: -</p> -<ul> -<li> the <a href="FAQ">FAQ</a> (please send any contributions) -<li> the <a href="userman">Proof General user manual</a> -</li> -<li> the <a href="adaptingman">Adapting Proof General manual</a> -</li> -</ul> -<p> -The second manual gives instructions on how to adapt Proof General to new -proof systems, it's not needed for ordinary use. -For printing you can download: -<ul> -<li> -<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "User manual [ps]") ?> and -<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "Adapting manual [ps]") ?>, or -</li> -<li> -<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "User manual [pdf]") ?>, -<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "Adapting manual [pdf]") ?> -</li> -</ul> -<p> -The PostScript files are recommended over the PDF. -Both manuals (HTML and Info formats) are included in the -<a href="download">download</a>. When running Proof General the manual -is available from the "Proof General" menu. It should also appear in -the system Info pages. -If you're considering developing Proof General, please check -that you are using the documentation for the most recent -development version of Proof General, available with the -<a href="develdownload">development download</a>. -</p> - -<p> -You can discuss Proof General with other users and receive -announcements by joining our <a href="mailinglist.html">mailing -list</a>. -</p> - - -<h2>Manuals for Emacs</h2> - -<p>If you're new to Emacs, it's recommended to try the Emacs tutorial, -available inside Emacs by pressing <b>C-h t</b> (which means -<tt>ctrl</tt>-with-<tt>h</tt> followed by <tt>t</tt>). There are many -other <b>C-h</b> commands, and the Help menu inside Emacs gives access -to more help facilities. -</p> -<p>For on-line reading, these links might be helpful: -<ul> -<li>The <a href="http://www.gnu.org/manual/emacs/">Emacs user manual</a></li> -<li>The <a href="http://www.gnu.org/manual/emacs-lisp-intro"> - Emacs lisp introduction</a> and - <a href="http://www.gnu.org/manual/elisp">Emacs lisp reference</a>.</li> -</li> -</ul> -(You don't need to look at anything about lisp unless you're interested -in developing Proof General). -</p> -<p>The corresponding manuals for XEmacs are -available <a href="http://www.xemacs.org/Documentation/index.html">here</a> (xemacs.org). -</p> - - - - - - -<h2>References</h2> - -<p> Ideas for the future of Proof General are given here: -</p> -<ul> -<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a> and - <a href="http://http://www.informatik.uni-bremen.de/~cxl/">Christoph Lüth</a> - <b><i>Proof General meets IsaWin</i></b>. - Proc. User Interfaces for Theorem Provers 2003 (UITP'03) September 2003, - Rome, Italy. - Available as <?php download_link("papers/uitp03.pdf", "[pdf]") ?>. -</li> - -<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. - <b><i>Protocols for Interactive e-Proof</i></b>. - Draft version, see - <a href="http://homepages.inf.ed.ac.uk/da/drafts/#eproof">here</a>. -</li> -<li><a href="http://homepages.inf.ed.ac.uk/da">David Aspinall</a>. - <b><i>Proof General Kit (white paper)</i></b>. - Draft version, see - <a href="http://homepages.inf.ed.ac.uk/da/drafts/#white">here</a>. -</li> -</ul> -<p> A technology overview of Proof General is given here: -</p> -<ul> -<li> <a href="http://homepages.inf.ed.ac.uk/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é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>, Thomas Kleymann-Schreiber and Dilip Sequeira. - <I>Implementing Proof by Pointing without a Structure Editor</I>. - LFCS Technical Report <a - href="http://www.lfcs.informatics.ed.ac.uk/reports/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> |