diff options
Diffstat (limited to 'html/doc.html')
| -rw-r--r-- | html/doc.html | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/html/doc.html b/html/doc.html new file mode 100644 index 00000000..3f092ade --- /dev/null +++ b/html/doc.html @@ -0,0 +1,107 @@ +<h2>Manual</h2> + +<p> +There are two manuals for Proof General: +</p> +<ul> +<li> the +<?php htmlshow("ProofGeneral-3.3/doc/ProofGeneral_toc.html","Proof General user manual ","Proof General Manual") ?> +</li> +<li> the +<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","Adapting Proof General manual","Adapting Proof General manual") ?> +</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. +</p> +<p> +For printing you can download: +<ul> +<li> +<?php download_link("ProofGeneral-3.3/doc/ProofGeneral.ps.gz", "User manual [ps]") ?> and +<?php download_link("ProofGeneral-3.3/doc/PG-adapting.ps.gz", "Adapting manual [ps]") ?>, or +</li> +<li> +<?php download_link("ProofGeneral-3.3/doc/ProofGeneral.pdf", "User manual [pdf]") ?>, +<?php download_link("ProofGeneral-3.3/doc/PG-adapting.pdf", "Adapting manual [pdf]") ?> +</li> +</ul> +<p> +The PostScript files are recommended over the PDF. +</p> +<p> +Note that both manuals (in 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. +</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>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é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.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> |