7 NEWS file in the distribution for more details. Some notable changes |
7 NEWS file in the distribution for more details. Some notable changes |
8 are: |
8 are: |
9 |
9 |
10 * Explicit proof terms for type class reasoning. |
10 * Explicit proof terms for type class reasoning. |
11 |
11 |
12 * Authentic syntax for *all* logical entities (type classes, type |
12 * Robust treatment of concrete syntax for different logical entities; |
13 constructors, term constants): provides simple and robust |
13 mixfix syntax in local proof context. |
14 correspondence between formal entities and concrete syntax. |
|
15 |
14 |
16 * HOL: Package for constructing quotient types. |
15 * Type declarations and notation within local theory context. |
17 |
16 |
18 * HOL: Code generation now with simple concept for abstract |
17 * HOL: package for quotient types. |
19 datatypes obeying invariants; applications for typical data structures |
|
20 (e.g. search trees) can be found in the library. |
|
21 |
18 |
22 * HOL: New development of the Reals using Cauchy Sequences. |
19 * HOL code generation: simple concept for abstract datatypes obeying |
|
20 invariants (e.g. red-black trees). |
23 |
21 |
24 * HOL: Reorganization of abstract algebra type class hierarchy. |
22 * HOL: new development of the Reals using Cauchy Sequences. |
25 |
23 |
26 * Commands 'types', 'typedecl' and 'typedef' now work within a local theory |
24 * HOL: reorganization of abstract algebra type class hierarchy. |
27 context -- without introducing dependencies on parameters or |
25 |
28 assumptions. |
26 * HOL: substantial reorganization of main library and related tools. |
|
27 |
|
28 * HOLCF: reorganization of 'domain' package. |
|
29 |
29 |
30 |
30 You may get Isabelle2009-2 from the following mirror sites: |
31 You may get Isabelle2009-2 from the following mirror sites: |
31 |
32 |
32 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
33 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ |
33 Munich (Germany) http://isabelle.in.tum.de/ |
34 Munich (Germany) http://isabelle.in.tum.de/ |