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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
<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
on 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://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>
|
