1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
<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 manual is available in HTML
<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","here.","Proof General Manual") ?>
<br>
For printing you can download the
<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "gzipped ps file") ?>.
<!-- <?php download_link("ProofGeneral/doc/ProofGeneral.dvi", "dvi") ?> -->
<!-- plus front page image -->
<!-- <?php download_link("ProofGeneral/doc/ProofGeneral.eps.eps", "gzipped eps") ?> -->
<!-- <?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "pdf") ?> -->
</p>
<p>
<it>Warning:</it> the manual 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é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>
|
