aboutsummaryrefslogtreecommitdiff
path: root/html
diff options
context:
space:
mode:
authorDavid Aspinall1999-10-21 15:45:29 +0000
committerDavid Aspinall1999-10-21 15:45:29 +0000
commit2111db37b99d87dd973996c9df1ce6b99ba56d0c (patch)
treea58ac70956615b2432a1f38bf4eb30c818f18ff0 /html
parenta01581bbc0d8e8170b85a4d18f437c1e090aa57d (diff)
Updated for new screenshot
Diffstat (limited to 'html')
-rw-r--r--html/features.phtml7
-rw-r--r--html/news.phtml5
-rw-r--r--html/screenshot.phtml9
3 files changed, 14 insertions, 7 deletions
diff --git a/html/features.phtml b/html/features.phtml
index 3e5e4c55..4dc01cef 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -66,9 +66,10 @@ assistant, and you'd like some of the following features:
</dd>
<?php dt("Toolbar.") ?>
<dd>
- Proof General has a toolbar with buttons for starting a proof,
- manoeuvring in the proof script, restarting the prover
- and saving a proof.
+ Proof General has a toolbar with buttons for examining
+ the proof state, starting a proof, manoeuvring in the proof script,
+ restarting the prover, saving a proof, searching for a theorem,
+ issuing a command, interrupting the assistant, and getting help.
<p>
Using the toolbar, you can replay proofs without knowing any
low-level commands of the proof assistant or any Emacs hot-keys!
diff --git a/html/news.phtml b/html/news.phtml
index 551c4bb9..a19189d1 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -4,6 +4,11 @@
</p>
<ul>
+<li><b>21st October 1999</b><br>
+ <p>
+ See what Proof General 3.0 will look like!
+ The <a href="screenshot.phtml>screenshot</a> has been updated.
+ </p>
<li><b>14th October 1999</b><br>
<p>
The next version of Proof General will be 3.0.
diff --git a/html/screenshot.phtml b/html/screenshot.phtml
index 0deeddff..0045db9c 100644
--- a/html/screenshot.phtml
+++ b/html/screenshot.phtml
@@ -3,8 +3,10 @@
small_header("Screenshot");
?>
<p>
-Below is a picture of Isabelle Proof General running inside XEmacs,
-replaying a simple proof.
+Below is a picture of Isabelle Proof General 3.0 running inside XEmacs.
+<br>
+We are replaying a proof in Isar, Isabelle's new proof language
+developed by Markus Wenzel.
</p>
<p>
The top half of the window displays the proof script.
@@ -17,8 +19,7 @@ sent to the proof process so far. It cannot be edited.
The bottom half of the window displays the output from Isabelle
at each stage of the proof.
</p>
-<img src="images/IsaPGscreen.jpg" ALT="Isabelle Proof General screenshot">
-
+<img src="images/pg-isar-screenshot.png" ALT="Isabelle Proof General screenshot [png support needed]">
<?php
click_to_go_back();
footer();