2 Isabelle |
2 Isabelle |
3 |
3 |
4 %body% |
4 %body% |
5 |
5 |
6 <p> |
6 <p> |
|
7 |
|
8 <h2>What is Isabelle?</h2> |
7 |
9 |
8 Isabelle is a popular generic theorem proving environment developed at |
10 Isabelle is a popular generic theorem proving environment developed at |
9 Cambridge University (<a |
11 Cambridge University (<a |
10 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
12 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
11 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
13 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
19 |
21 |
20 <li> <a |
22 <li> <a |
21 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
23 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
22 at Cambridge</strong></a> |
24 at Cambridge</strong></a> |
23 |
25 |
24 <li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle |
26 <li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle at Munich</strong></a> |
25 at Munich</strong></a> |
|
26 |
27 |
27 </ul> |
28 </ul> |
28 |
29 |
29 See there for information on projects done with Isabelle, mailing list |
30 See there for information on projects done with Isabelle, mailing list |
30 archives, research papers, the Isabelle bibliography, and Isabelle |
31 archives, research papers, the Isabelle bibliography, and Isabelle |
31 workshops and courses. |
32 workshops and courses. |
32 |
33 |
|
34 <p> |
33 |
35 |
34 <h2>Obtaining Isabelle</h2> |
36 <h2>Obtaining Isabelle</h2> |
|
37 |
|
38 You get <strong><!-- _GP_ distname --></strong> in the |
|
39 <a href="dist/index.html">distribution area</a>. |
|
40 |
|
41 <p> |
35 |
42 |
36 The <strong><!-- _GP_ distname --></strong> distribution is available |
43 The <strong><!-- _GP_ distname --></strong> distribution is available |
37 from several <a href="dist/index.html">mirror sites</a>. It includes |
44 from several <a href="dist/index.html">mirror sites</a>. It includes |
38 source and binary packages and browsable documentation. |
45 source and binary packages and browsable documentation. |
39 |
46 |
44 href="library/HOL/index.html">HOL</a>, <a |
51 href="library/HOL/index.html">HOL</a>, <a |
45 href="library/HOLCF/index.html">HOLCF</a>, <a |
52 href="library/HOLCF/index.html">HOLCF</a>, <a |
46 href="library/FOL/index.html">FOL</a> and <a |
53 href="library/FOL/index.html">FOL</a> and <a |
47 href="library/ZF/index.html">ZF</a>. |
54 href="library/ZF/index.html">ZF</a>. |
48 |
55 |
|
56 <p> |
49 |
57 |
50 <h2>Mailing list</h2> |
58 <h2>Mailing list</h2> |
51 |
59 |
52 Use the mailing list <a href="mailto: |
60 Use the mailing list <a href="mailto: |
53 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to |
61 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
|
62 and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to |
54 discuss problems and results. Why not <A |
63 discuss problems and results. Why not <A |
55 HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? |
64 HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? |
|
65 |