diff options
Diffstat (limited to 'html/doc.html')
| -rw-r--r-- | html/doc.html | 132 |
1 files changed, 132 insertions, 0 deletions
diff --git a/html/doc.html b/html/doc.html new file mode 100644 index 00000000..7be1ba5f --- /dev/null +++ b/html/doc.html @@ -0,0 +1,132 @@ +<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>. + <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> |