%title%
Isabelle
%body%
<p>
<h2>Isabelle</h2>
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.
<p>
<h2>Obtaining Isabelle</h2>
Visit the <a href="dist/">download page</a>.
<p>
Several mirror sites provide the Isabelle <a
href="dist/">distribution</a>, which includes <a
href="dist/source.html">sources</a>, <a
href="dist/binary.html">binary packages</a>, and <a
href="dist/docs.html">documentation</a>.
The current version is <strong><!-- _GP_ distname --></strong>.
<p>
You can also browse the main Isabelle logics
<a href="library/HOL/">HOL</a>, <a href="library/HOLCF/">HOLCF</a>,
<a href="library/FOL/">FOL</a> and <a href="library/ZF/">ZF</a> online.
<p>
<h2>User interface</h2>
The distribution includes only a very primitive interface based on
ordinary terminal sessions.
<p>
<a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is
a generic Emacs interface for proof assistants, including Isabelle
(both for the classic and Isar version). Proof General is suitable
for use by pacifists and Emacs militants alike. Its most prominent
feature is script management, providing a metaphor of <em>live proof
script editing</em>.
<p>
<h2>Mailing list</h2>
Use the mailing list <a href="mailto:
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
discuss problems and results.
(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)