author | paulson |
Tue, 10 Feb 2004 12:17:04 +0100 | |
changeset 14379 | ea10a8c3e9cf |
parent 14230 | def0606302a1 |
child 14576 | 37a92211a5d3 |
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@10050 | 8 |
<h2>What is Isabelle?</h2> |
kleing@10050 | 9 |
|
wenzelm@10019 | 10 |
Isabelle is a popular generic theorem proving environment developed at |
wenzelm@10019 | 11 |
Cambridge University (<a |
kleing@8056 | 12 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
kleing@8056 | 13 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
berghofe@14230 | 14 |
See the <a href="overview.html">Isabelle overview</a>. |
kleing@8056 | 15 |
|
kleing@8056 | 16 |
<p> |
kleing@8056 | 17 |
|
kleing@9285 | 18 |
These pages provide general information on Isabelle, more specific |
kleing@8056 | 19 |
information is available from the local pages |
kleing@8056 | 20 |
|
kleing@8056 | 21 |
<ul> |
kleing@8056 | 22 |
|
wenzelm@11109 | 23 |
<li><a |
kleing@8056 | 24 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
wenzelm@11109 | 25 |
at Cambridge</strong></a> |
kleing@8056 | 26 |
|
kleing@13087 | 27 |
<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle |
wenzelm@11109 | 28 |
at Munich</strong></a> |
kleing@8056 | 29 |
|
kleing@8056 | 30 |
</ul> |
kleing@8056 | 31 |
|
kleing@8056 | 32 |
See there for information on projects done with Isabelle, mailing list |
kleing@8056 | 33 |
archives, research papers, the Isabelle bibliography, and Isabelle |
kleing@8056 | 34 |
workshops and courses. |
kleing@8056 | 35 |
|
kleing@10050 | 36 |
<p> |
kleing@8056 | 37 |
|
kleing@13087 | 38 |
<h2>Out now</h2> |
kleing@13087 | 39 |
|
kleing@13087 | 40 |
The |
kleing@13087 | 41 |
<a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> -- |
kleing@13087 | 42 |
published by Springer Verlag as <a |
kleing@13087 | 43 |
href="http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>. |
kleing@13087 | 44 |
|
kleing@13087 | 45 |
<p> |
kleing@13087 | 46 |
|
kleing@8056 | 47 |
<h2>Obtaining Isabelle</h2> |
kleing@8056 | 48 |
|
wenzelm@10041 | 49 |
The <strong><!-- _GP_ distname --></strong> distribution is available |
wenzelm@10041 | 50 |
from several <a href="dist/index.html">mirror sites</a>. It includes |
kleing@13848 | 51 |
source and binary packages and browsable documentation. There is also |
kleing@13848 | 52 |
a nightly generated <a href="http://isabelle.in.tum.de/devel/">development |
kleing@13848 | 53 |
snapshot</a> available. |
kleing@8056 | 54 |
|
kleing@8056 | 55 |
<p> |
kleing@9285 | 56 |
|
wenzelm@10019 | 57 |
You can also browse the <a href="library/index.html">Isabelle theory |
wenzelm@10019 | 58 |
library</a>; the main logics are <a |
wenzelm@10019 | 59 |
href="library/HOL/index.html">HOL</a>, <a |
wenzelm@10019 | 60 |
href="library/HOLCF/index.html">HOLCF</a>, <a |
wenzelm@10019 | 61 |
href="library/FOL/index.html">FOL</a> and <a |
wenzelm@10019 | 62 |
href="library/ZF/index.html">ZF</a>. |
kleing@8070 | 63 |
|
kleing@10050 | 64 |
<p> |
kleing@8056 | 65 |
|
kleing@8056 | 66 |
<h2>Mailing list</h2> |
kleing@8056 | 67 |
|
kleing@8056 | 68 |
Use the mailing list <a href="mailto: |
kleing@10050 | 69 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
paulson@14379 | 70 |
and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to |
wenzelm@10162 | 71 |
discuss problems and results. Why not <a |
wenzelm@10162 | 72 |
href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? |
kleing@10050 | 73 |