1 files changed, 115 insertions, 0 deletions
diff --git a/html/screenshot.html b/html/screenshot.html
new file mode 100644
index 00000000..ffc9e8a4
--- /dev/null
+++ b/html/screenshot.html
@@ -0,0 +1,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>
+