author | wenzelm |
Thu, 28 Sep 2000 23:00:55 +0200 | |
changeset 10114 | b07ed0c2f89f |
parent 10050 | c8e0bd7a1e9c |
child 10162 | 947b7b8b0a69 |
permissions | -rw-r--r-- |
8056 | 1 |
%title% |
2 |
Isabelle |
|
3 |
||
4 |
%body% |
|
5 |
||
6 |
<p> |
|
7 |
||
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
8 |
<h2>What is Isabelle?</h2> |
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
9 |
|
10019 | 10 |
Isabelle is a popular generic theorem proving environment developed at |
11 |
Cambridge University (<a |
|
8056 | 12 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
13 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
|
14 |
||
15 |
<p> |
|
16 |
||
9285 | 17 |
These pages provide general information on Isabelle, more specific |
8056 | 18 |
information is available from the local pages |
19 |
||
20 |
<ul> |
|
21 |
||
22 |
<li> <a |
|
23 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
|
24 |
at Cambridge</strong></a> |
|
25 |
||
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
26 |
<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle at Munich</strong></a> |
8056 | 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 |
||
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
34 |
<p> |
8056 | 35 |
|
36 |
<h2>Obtaining Isabelle</h2> |
|
37 |
||
10041 | 38 |
The <strong><!-- _GP_ distname --></strong> distribution is available |
39 |
from several <a href="dist/index.html">mirror sites</a>. It includes |
|
40 |
source and binary packages and browsable documentation. |
|
8056 | 41 |
|
42 |
<p> |
|
9285 | 43 |
|
10019 | 44 |
You can also browse the <a href="library/index.html">Isabelle theory |
45 |
library</a>; the main logics are <a |
|
46 |
href="library/HOL/index.html">HOL</a>, <a |
|
47 |
href="library/HOLCF/index.html">HOLCF</a>, <a |
|
48 |
href="library/FOL/index.html">FOL</a> and <a |
|
49 |
href="library/ZF/index.html">ZF</a>. |
|
8070 | 50 |
|
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
51 |
<p> |
8056 | 52 |
|
53 |
<h2>Mailing list</h2> |
|
54 |
||
55 |
Use the mailing list <a href="mailto: |
|
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
56 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
57 |
and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to |
10016 | 58 |
discuss problems and results. Why not <A |
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
59 |
HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? |
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
60 |