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
|
<p>
Here are some screenshots of Proof General 3.0 running with
different theorem provers. To see the full-size version
of a picture, click on its thumbnail.
</p>
<!-- FIXME: update pictures. Fix vertical centering of screenshots. -->
<table width="80%">
<tr>
<td width="200">
<a href="images/pg-lego-screenshot.png">
<img src="images/pg-lego-thumb.png" alt="LEGO Proof General" width=128 height=109 border=0>
</a>
</td>
<td>
<p><font size="-1">
Building a simple proof in LEGO with proof-by-pointing.
<br>
The top half of the window displays the proof script.
The bottom displays the output from LEGO at each
stage of the proof. Here, it shows
the current subgoals to be solved.
The part of the proof already processed by LEGO
has a blue background.
<br>
Clicking on terms in the subgoals list generates
commands which are added to the proof script.
</font></p>
<br>
</td></tr>
<tr>
<td width="200">
<a href="images/pg-coq-screenshot.png">
<img src="images/pg-coq-thumb.png" alt="Coq Proof General" width=153 height=115 border=0>
</a>
</td>
<td>
<p><font size="-1">
Coq Proof General running in multiple frame mode,
full screen shot (1024x768).
<br>
There are separate windows on the screen
for the script, goals, and response buffers.
In this picture, you can see Proof General's
indication that Coq is processing the
induction step, because the background of
the proof step is pink. It will become
blue when Coq finishes that step.
</font></p>
<br>
</td></tr>
<tr>
<td width="200">
<a href="images/pg-isa-screenshot.png">
<img src="images/pg-isa-thumb.png" alt="Isabelle Proof General" width=150 height=142 border=0>
</a>
</td>
<td>
<p><font size="-1">
Replaying a domain theory proof in Isabelle's HOLCF logic.
<br>
In Isabelle, theory files as well as ML files are coloured.
Proof General has some functions for processing and
undoing theory files, but most operations it provides
are for writing proof scripts in ML files.
<br>
Isabelle supports input and output in tokens which
display as symbols using the
<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
package in conjunction with Proof General.
Here you can see some symbols in Isabelle's output.
</font></p>
<br>
</td></tr>
<tr>
<td width="200">
<a href="images/pg-isar-screenshot.png">
<img src="images/pg-isar-thumb.png" alt="Isabelle/Isar Proof General" width=150 height=142 border=0>
</a>
</td>
<td>
<p><font size="-1">
Replaying a proof in Isar, Isabelle's declarative proof language
developed by Markus Wenzel.
</font></p>
<br>
</td></tr>
<tr>
<td width="200">
<a href="images/pg-lego-console.png">
<img src="images/pg-lego-console-thumb.png" alt="LEGO Proof General (console)" width=174 height=65 border=0>
</a>
</td>
<td>
<p><font size="-1">
LEGO Proof General running in plain console mode.
<br>
This shows that you can run Proof General even if sometimes
you need to use a plain tty or xterminal. Of course, the
graphical features are reduced!
</font></p>
<br>
</td>
</tr>
</table>
<p>
For more pictures, see the Proof General <a href="gallery">gallery</a>.
</p>
|
