author wenzelm
Thu, 28 Sep 2000 23:00:55 +0200
changeset 10114 b07ed0c2f89f
parent 10050 c8e0bd7a1e9c
child 10162 947b7b8b0a69
permissions -rw-r--r--




<h2>What is Isabelle?</h2>

Isabelle 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>

The <strong><!-- _GP_ distname --></strong> distribution is available
from several <a href="dist/index.html">mirror sites</a>.  It includes
source and binary packages and browsable documentation.


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


<h2>Mailing list</h2>

Use the mailing list <a href="mailto:"></a> 
and its <a href="">archive</a> to
discuss problems and results.  Why not <A