8056
|
1 |
%title%
|
|
2 |
Isabelle
|
|
3 |
|
|
4 |
%body%
|
|
5 |
|
|
6 |
<p>
|
|
7 |
|
|
8 |
<h2>Isabelle</h2>
|
|
9 |
is a popular generic theorem proving
|
|
10 |
environment developed at Cambridge University (<a
|
|
11 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
|
|
12 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
|
|
13 |
|
|
14 |
<p>
|
|
15 |
|
8070
|
16 |
These pages provide <a href="about.html">general information on Isabelle</a>, more specific
|
8056
|
17 |
information is available from the local pages
|
|
18 |
|
|
19 |
<ul>
|
|
20 |
|
|
21 |
<li> <a
|
|
22 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
|
|
23 |
at Cambridge</strong></a>
|
|
24 |
|
8060
|
25 |
<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle
|
8056
|
26 |
at Munich</strong></a>
|
|
27 |
|
|
28 |
</ul>
|
|
29 |
|
|
30 |
See there for information on projects done with Isabelle, mailing list
|
|
31 |
archives, research papers, the Isabelle bibliography, and Isabelle
|
|
32 |
workshops and courses.
|
|
33 |
|
|
34 |
<p>
|
|
35 |
|
|
36 |
|
|
37 |
<h2>Obtaining Isabelle</h2>
|
|
38 |
|
8221
|
39 |
Visit the <a href="dist/">download page</a>.
|
|
40 |
<p>
|
|
41 |
Several mirror sites provide the Isabelle <a
|
|
42 |
href="dist/">distribution</a>, which includes <a
|
|
43 |
href="dist/source.html">sources</a>, <a
|
|
44 |
href="dist/binary.html">binary packages</a>, and <a
|
|
45 |
href="dist/docs.html">documentation</a>.
|
|
46 |
The current version is <strong>{ISABELLE}</strong>.
|
8056
|
47 |
|
|
48 |
<p>
|
|
49 |
|
|
50 |
|
8070
|
51 |
<h2>User interface</h2>
|
|
52 |
|
|
53 |
The distribution includes only a very primitive interface based on
|
|
54 |
ordinary terminal sessions.
|
|
55 |
|
|
56 |
<p>
|
|
57 |
|
|
58 |
<a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is
|
|
59 |
a generic Emacs interface for proof assistants, including Isabelle
|
|
60 |
(both for the classic and Isar version). Proof General is suitable
|
|
61 |
for use by pacifists and Emacs militants alike. Its most prominent
|
|
62 |
feature is script management, providing a metaphor of <em>live proof
|
|
63 |
script editing</em>.
|
|
64 |
|
|
65 |
<p>
|
|
66 |
|
8056
|
67 |
|
|
68 |
<h2>Mailing list</h2>
|
|
69 |
|
|
70 |
Use the mailing list <a href="mailto:
|
|
71 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
|
|
72 |
discuss problems and results.
|
|
73 |
(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
|