| author | kleing |
| Thu, 09 Dec 1999 13:11:12 +0100 | |
| changeset 8060 | 8444b282a7a7 |
| parent 8056 | 3c587e7b8fe5 |
| child 8070 | dbbef2367723 |
| permissions | -rw-r--r-- |
| kleing@8056 | 1 |
%title% |
| kleing@8056 | 2 |
Isabelle |
| kleing@8056 | 3 |
|
| kleing@8056 | 4 |
%body% |
| kleing@8056 | 5 |
|
| kleing@8056 | 6 |
<p> |
| kleing@8056 | 7 |
|
| kleing@8056 | 8 |
<h2>Isabelle</h2> |
| kleing@8056 | 9 |
is a popular generic theorem proving |
| kleing@8056 | 10 |
environment developed at Cambridge University (<a |
| kleing@8056 | 11 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
| kleing@8056 | 12 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
| kleing@8056 | 13 |
|
| kleing@8056 | 14 |
<p> |
| kleing@8056 | 15 |
|
| kleing@8056 | 16 |
This page provides general information on Isabelle, more specific |
| kleing@8056 | 17 |
information is available from the local pages |
| kleing@8056 | 18 |
|
| kleing@8056 | 19 |
<ul> |
| kleing@8056 | 20 |
|
| kleing@8056 | 21 |
<li> <a |
| kleing@8056 | 22 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
| kleing@8056 | 23 |
at Cambridge</strong></a> |
| kleing@8056 | 24 |
|
| kleing@8060 | 25 |
<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle |
| kleing@8056 | 26 |
at Munich</strong></a> |
| kleing@8056 | 27 |
|
| kleing@8056 | 28 |
</ul> |
| kleing@8056 | 29 |
|
| kleing@8056 | 30 |
See there for information on projects done with Isabelle, mailing list |
| kleing@8056 | 31 |
archives, research papers, the Isabelle bibliography, and Isabelle |
| kleing@8056 | 32 |
workshops and courses. |
| kleing@8056 | 33 |
|
| kleing@8056 | 34 |
<p> |
| kleing@8056 | 35 |
|
| kleing@8056 | 36 |
|
| kleing@8056 | 37 |
<h2>Obtaining Isabelle</h2> |
| kleing@8056 | 38 |
|
| kleing@8056 | 39 |
The current version is <strong>{ISABELLE}</strong>. Several mirror
|
| kleing@8056 | 40 |
sites provide the Isabelle <a href="dist/">distribution</a>, which |
| kleing@8056 | 41 |
includes sources, documentation, and binary packages. |
| kleing@8056 | 42 |
|
| kleing@8056 | 43 |
|
| kleing@8056 | 44 |
<p> |
| kleing@8056 | 45 |
|
| kleing@8056 | 46 |
|
| kleing@8056 | 47 |
|
| kleing@8056 | 48 |
<h2>Mailing list</h2> |
| kleing@8056 | 49 |
|
| kleing@8056 | 50 |
Use the mailing list <a href="mailto: |
| kleing@8056 | 51 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to |
| kleing@8056 | 52 |
discuss problems and results. |
| kleing@8056 | 53 |
(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?) |