blob: b76a61efebfa682f2e1820adb3910ed80c2a0e68 (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
"http://www.w3.org/TR/REC-html40/loose.dtd">
<html>
<head>
<title>Proof General --- Organize your proof with Emacs</title>
<META NAME="author" CONTENT="David Aspinall <da@dcs.ed.ac.uk>">
<META NAME="keywords" CONTENT="Isabelle, LEGO, Coq, Emacs, XEmacs,
Interface, Theorem Prover, GUI, David Aspinall">
<META NAME="description" CONTENT="Proof General is an Emacs based
generic interface for theorem provers">
</head>
<BODY
BGCOLOR="#500030"
TEXT="#FFFFFF"
LINK="#A0D0FF"
VLINK="#A0D080"
ALINK="#FFD000"
>
<HR>
<TABLE WIDTH="80%">
<TR>
<TD WIDTH="50%"><A HREF="http://www.dcs.ed.ac.uk/proofgen"><IMG SRC="ProofGeneral.jpg" ALT="[ Proof General logo (subject to change!) ]" ></A></TD>
<TD WIDTH="50%">
<H1>
<h1>Proof General</h1>
<h3>Isabelle Screenshot</h3>
</TR>
</TABLE>
<HR>
<p>
<img src="IsaPGscreen.jpg">
<p>
This is a picture of Isabelle Proof General running inside XEmacs,
replaying a simple proof.
<br>
The top half of the window displays the proof script.
<br>
The blue highlighted region is the part of the script which has been
sent to the proof process so far. It cannot be edited.
<br>
The bottom half of the window displays the output from Isabelle
at each stage of the proof.
<hr>
<A HREF="http://validator.w3.org/check?uri=http://www.dcs.ed.ac.uk/proofgen/IsabePGscreen.html;pw;ss"><IMG BORDER=0
SRC="vh40.gif"
ALT="Valid HTML 4.0!" HEIGHT=31 WIDTH=88 ALIGN=right></A>
<address><a href="mailto:proofgen@dcs.ed.ac.uk">Proof General maintainer</a></address>
<!-- Created: Fri Oct 2 16:18:24 BST 1998 -->
<!-- hhmts start -->
Last modified: Fri Oct 2 16:31:11 BST 1998
<!-- hhmts end -->
</body>
</html>
|
