8 <h2>What is Isabelle?</h2>
10 Isabelle is a popular generic theorem proving environment developed at
11 Cambridge University (<a
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 See the <a href="overview.html">Isabelle overview</a>.
18 These pages provide general information on Isabelle, more specific
19 information is available from the local pages
24 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
25 at Cambridge</strong></a>
27 <li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
28 at Munich</strong></a>
32 See there for information on projects done with Isabelle, mailing list
33 archives, research papers, the Isabelle bibliography, and Isabelle
34 workshops and courses.
41 <a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> --
42 published by Springer Verlag as <a
43 href="http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>.
47 <h2>Obtaining Isabelle</h2>
49 The <strong><!-- _GP_ distname --></strong> distribution is available
50 from several <a href="dist/index.html">mirror sites</a>. It includes
51 source and binary packages and browsable documentation. There is also
52 a nightly generated <a href="http://isabelle.in.tum.de/devel/">development
53 snapshot</a> available.
57 You can also browse the <a href="library/index.html">Isabelle theory
58 library</a>; the main logics are <a
59 href="library/HOL/index.html">HOL</a>, <a
60 href="library/HOLCF/index.html">HOLCF</a>, <a
61 href="library/FOL/index.html">FOL</a> and <a
62 href="library/ZF/index.html">ZF</a>.
68 Use the mailing list <a href="mailto:
69 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
70 and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
71 discuss problems and results. Why not <a
72 href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?