author | kleing |
Mon, 19 Apr 2004 08:20:52 +0200 | |
changeset 14624 | 9b3397a848c3 |
parent 14615 | 603f08285c65 |
child 14637 | d258f6c11d83 |
permissions | -rw-r--r-- |
8056 | 1 |
%title% |
2 |
Isabelle |
|
3 |
||
4 |
%body% |
|
5 |
||
6 |
<p> |
|
7 |
||
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
8 |
<h2>What is Isabelle?</h2> |
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
9 |
|
10019 | 10 |
Isabelle is a popular generic theorem proving environment developed at |
11 |
Cambridge University (<a |
|
8056 | 12 |
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU |
13 |
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>). |
|
14230 | 14 |
See the <a href="overview.html">Isabelle overview</a>. |
8056 | 15 |
|
16 |
<p> |
|
17 |
||
9285 | 18 |
These pages provide general information on Isabelle, more specific |
8056 | 19 |
information is available from the local pages |
20 |
||
21 |
<ul> |
|
22 |
||
11109 | 23 |
<li><a |
8056 | 24 |
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle |
11109 | 25 |
at Cambridge</strong></a> |
8056 | 26 |
|
13087 | 27 |
<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle |
11109 | 28 |
at Munich</strong></a> |
8056 | 29 |
|
30 |
</ul> |
|
31 |
||
32 |
See there for information on projects done with Isabelle, mailing list |
|
33 |
archives, research papers, the Isabelle bibliography, and Isabelle |
|
34 |
workshops and courses. |
|
35 |
||
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
36 |
<p> |
8056 | 37 |
|
14576 | 38 |
<h2><!-- _GP_ distname --></h2> |
39 |
New features in <strong><!-- _GP_ distname --></strong> include |
|
40 |
<ul> |
|
14624 | 41 |
<li>New image HOL4 with imported library from HOL4 system on top of |
42 |
HOL-Complex (about 2500 additional theorems).</li> |
|
43 |
||
14576 | 44 |
<li>New theory Ring_and_Field with over 250 basic numerical laws, |
45 |
all proved in axiomatic type classes for semirings, rings and fields.</li> |
|
46 |
||
47 |
<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li> |
|
48 |
||
49 |
<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li> |
|
50 |
||
14611 | 51 |
<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li> |
52 |
||
14576 | 53 |
<li>Improved locales (named proof contexts), instantiation of locales.</li> |
54 |
||
55 |
<li>Improved handling of linear and partial orders in simplifier.</li> |
|
56 |
||
57 |
<li>New <code>specification</code> command for definition by specification.</li> |
|
58 |
||
59 |
<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li> |
|
60 |
||
61 |
<li><code>arith</code> now generates counterexamples for reals as well.</li> |
|
62 |
||
14580 | 63 |
<li>New <code>quickcheck</code> command |
14615 | 64 |
to search for counterexamples of executable goals. |
65 |
(see HOL/ex/Quickcheck_Examples.thy)</li> |
|
14580 | 66 |
<li>New <code>refute</code> command |
14615 | 67 |
to search for finite countermodels of goals. |
68 |
(see HOL/ex/Refute_Examples.thy) |
|
69 |
</li> |
|
14576 | 70 |
|
14615 | 71 |
<li>Presentation and x-symbol enhancements, greek letters and |
72 |
sub/superscripts allowed in identifiers.</li> |
|
14576 | 73 |
</ul> |
74 |
<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a> |
|
75 |
<p> |
|
76 |
The <strong><!-- _GP_ distname --></strong> distribution is available |
|
77 |
from several <a href="dist/index.html">mirror sites</a>. It includes |
|
78 |
source and binary packages and browsable documentation. There is also |
|
79 |
a nightly generated <a href="http://isabelle.in.tum.de/devel/">development |
|
80 |
snapshot</a> available. |
|
81 |
||
82 |
<p> |
|
83 |
||
13087 | 84 |
<h2>Out now</h2> |
85 |
||
86 |
The |
|
87 |
<a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> -- |
|
88 |
published by Springer Verlag as <a |
|
89 |
href="http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>. |
|
90 |
||
91 |
<p> |
|
92 |
||
10019 | 93 |
You can also browse the <a href="library/index.html">Isabelle theory |
94 |
library</a>; the main logics are <a |
|
95 |
href="library/HOL/index.html">HOL</a>, <a |
|
96 |
href="library/HOLCF/index.html">HOLCF</a>, <a |
|
97 |
href="library/FOL/index.html">FOL</a> and <a |
|
98 |
href="library/ZF/index.html">ZF</a>. |
|
8070 | 99 |
|
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
100 |
<p> |
8056 | 101 |
|
102 |
<h2>Mailing list</h2> |
|
103 |
||
104 |
Use the mailing list <a href="mailto: |
|
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
105 |
isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> |
14379 | 106 |
and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to |
10162 | 107 |
discuss problems and results. Why not <a |
108 |
href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? |
|
10050
c8e0bd7a1e9c
added headline, "quick download", and mailing list archive
kleing
parents:
10041
diff
changeset
|
109 |