Deleted file

1 files changed, 0 insertions, 115 deletions

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