diff options
| author | David Aspinall | 1999-10-21 15:45:29 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-21 15:45:29 +0000 |
| commit | 2111db37b99d87dd973996c9df1ce6b99ba56d0c (patch) | |
| tree | a58ac70956615b2432a1f38bf4eb30c818f18ff0 /html | |
| parent | a01581bbc0d8e8170b85a4d18f437c1e090aa57d (diff) | |
Updated for new screenshot
Diffstat (limited to 'html')
| -rw-r--r-- | html/features.phtml | 7 | ||||
| -rw-r--r-- | html/news.phtml | 5 | ||||
| -rw-r--r-- | html/screenshot.phtml | 9 |
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(); |
