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