%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 <a href="about.html">general information on Isabelle</a>, 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>{ISABELLE}</strong>.

 <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>?)