author wenzelm
Wed, 13 Sep 2000 22:49:17 +0200
changeset 9954 734e0ec40f44
parent 9920 9734f2717203
child 10016 3833b58a5d88
permissions -rw-r--r--
dummy (generated by makedist);




is a popular generic theorem proving
environment developed at Cambridge University (<a
href="">Larry Paulson</a>) and TU
Munich (<a href="">Tobias Nipkow</a>).


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


<li> <a
at Cambridge</strong></a> 

<li> <a href=""><strong>Isabelle
at Munich</strong></a>


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>

Visit the <a href="dist/">download page</a>.
  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
  The current version is <strong><!-- _GP_ distname --></strong>.


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.


<h2>User interface</h2>

The distribution includes only a very primitive interface based on
ordinary terminal sessions.


<a href="">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>.


<h2>Mailing list</h2>

Use the mailing list <a href="mailto:"></a> to
discuss problems and results.  
(Why not <A HREF="">subscribe</A>?)