blob: 0045db9c3679258ea467d0fbbc5291099db8e238 (
plain)
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
|
<?php
require('functions.php3');
small_header("Screenshot");
?>
<p>
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.
</p>
<p>
The blue highlighted region is the part of the script which has been
sent to the proof process so far. It cannot be edited.
</p>
<p>
The bottom half of the window displays the output from Isabelle
at each stage of the proof.
</p>
<img src="images/pg-isar-screenshot.png" ALT="Isabelle Proof General screenshot [png support needed]">
<?php
click_to_go_back();
footer();
?>
|
