Admin/page/main-content/index.content

tuned;

%title%
Isabelle

%body%

<p>

Isabelle is a popular generic theorem proving environment developed at
Cambridge University (<a
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).

<p>

These pages provide general information on Isabelle, more specific
information is available from the local pages

<ul>

<li> <a
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
at Cambridge</strong></a> 

<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle
at Munich</strong></a>

</ul>

See there for information on projects done with Isabelle, mailing list
archives, research papers, the Isabelle bibliography, and Isabelle
workshops and courses.


<h2>Obtaining Isabelle</h2>

Several mirror sites provide the Isabelle <a
href="dist/index.html">distribution</a>, which includes source and
binary <a href="dist/packages.html">packages</a> and browsable <a
href="dist/docs.html">documentation</a>.  The current version is
<strong><!-- _GP_ distname --></strong>.

<p>

You can also browse the <a href="library/index.html">Isabelle theory
library</a>; the main logics are <a
href="library/HOL/index.html">HOL</a>, <a
href="library/HOLCF/index.html">HOLCF</a>, <a
href="library/FOL/index.html">FOL</a> and <a
href="library/ZF/index.html">ZF</a>.


<h2>Mailing list</h2>

Use the mailing list <a href="mailto:
[e-mail]">[e-mail]</a> to
discuss problems and results.  Why not <A
HREF="mailto:[e-mail]">subscribe</A>?