| author | schirmer |
| Tue, 30 May 2006 12:24:04 +0200 | |
| changeset 19750 | 5281bd607206 |
| parent 19652 | f0594a06f2f0 |
| permissions | -rw-r--r-- |
| 16233 | 1 |
<?xml version='1.0' encoding='iso-8859-1' ?> |
2 |
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
|
| 16240 | 3 |
<!-- $Id$ --> |
| 16233 | 4 |
<html xmlns="http://www.w3.org/1999/xhtml"> |
5 |
||
6 |
<head> |
|
7 |
<title>Isabelle</title> |
|
8 |
<?include file="//include/htmlheader.include.html"?> |
|
9 |
</head> |
|
10 |
||
11 |
<body class="main"> |
|
12 |
<?include file="//include/header.include.html"?> |
|
13 |
<div class="hr"><hr/></div> |
|
14 |
<?include file="//include/navigation.include.html"?> |
|
15 |
<div class="hr"><hr/></div> |
|
16 |
<div id="content"> |
|
17 |
<h2>What is Isabelle?</h2> |
|
18 |
<p> |
|
19 |
Isabelle is a popular generic theorem proving environment |
|
20 |
developed at Cambridge University (<a |
|
21 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) |
|
22 |
and TU Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias |
|
23 |
Nipkow</a>). See the <a href="overview.html">Isabelle |
|
24 |
overview</a>. |
|
25 |
</p> |
|
26 |
<p> |
|
| 17143 | 27 |
This site provides general information on Isabelle, more |
| 16300 | 28 |
specific information is available from the local sites |
| 16233 | 29 |
</p> |
30 |
||
31 |
<ul> |
|
32 |
||
33 |
<li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
|
34 |
at Cambridge</strong></a></li> |
|
35 |
||
36 |
<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle |
|
37 |
at Munich</strong></a></li> |
|
38 |
||
39 |
</ul> |
|
40 |
||
41 |
<p> |
|
42 |
See there for information on projects done with Isabelle, |
|
43 |
mailing list archives, research papers, the Isabelle |
|
44 |
bibliography, and Isabelle workshops and courses. |
|
45 |
</p> |
|
46 |
||
| 17731 | 47 |
<h2>Now available: Isabelle2005</h2> |
| 17692 | 48 |
<p>Some highlights:</p> |
| 16233 | 49 |
<ul> |
| 19094 | 50 |
<li>Interpretation of locale expressions in theories, locales, and proof contexts.</li> |
51 |
<li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li> |
|
52 |
<li>Proof tools for transitivity reasoning.</li> |
|
53 |
<li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li> |
|
54 |
<li>Commands for generating adhoc draft documents.</li> |
|
55 |
<li>Support for Unicode proof documents (UTF-8).</li> |
|
56 |
<li>Major internal reorganizations and performance improvements.</li> |
|
57 |
</ul> |
|
| 16233 | 58 |
|
| 17671 | 59 |
<p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p> |
| 16233 | 60 |
|
61 |
<h2>Download</h2> |
|
62 |
||
63 |
<p> |
|
| 17661 | 64 |
Isabelle is distributed for free under the BSD license. It includes |
65 |
source and binary packages and browsable documentation, see the <a |
|
66 |
href="installation.html">installation instructions</a>. You can also |
|
67 |
browse the <a href="//dist/library/index.html">Isabelle theory |
|
68 |
library</a> online. |
|
| 16233 | 69 |
</p> |
70 |
||
71 |
<p> |
|
| 16927 | 72 |
Use the mailing list <a href= |
73 |
"mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its |
|
| 19094 | 74 |
<a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html">archive</a> to |
| 19533 | 75 |
discuss problems and results. |
|
19652
f0594a06f2f0
replaced references to the robot by the mailing list page
paulson
parents:
19554
diff
changeset
|
76 |
Why not <a href="https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users">subscribe</a>? |
| 16233 | 77 |
</p> |
78 |
||
79 |
</div> |
|
80 |
<div class="hr"><hr/></div> |
|
81 |
<?include file="//include/footer.include.html"?> |
|
82 |
</body> |
|
83 |
||
84 |
</html> |