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 |
|
|
16 |
This page provides general information on Isabelle, more specific
|
|
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 |
|
|
25 |
<li> <a href="munich.html"><strong>Isabelle
|
|
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 |
|
|
39 |
The current version is <strong>{ISABELLE}</strong>. Several mirror
|
|
40 |
sites provide the Isabelle <a href="dist/">distribution</a>, which
|
|
41 |
includes sources, documentation, and binary packages.
|
|
42 |
|
|
43 |
|
|
44 |
<p>
|
|
45 |
|
|
46 |
|
|
47 |
|
|
48 |
<h2>Mailing list</h2>
|
|
49 |
|
|
50 |
Use the mailing list <a href="mailto:
|
|
51 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
|
|
52 |
discuss problems and results.
|
|
53 |
(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
|