2 Subject: Announcing Isabelle2002 |
2 Subject: Announcing Isabelle2002 |
3 To: isabelle-users@cl.cam.ac.uk |
3 To: isabelle-users@cl.cam.ac.uk |
4 |
4 |
5 Isabelle2002 is now available. |
5 Isabelle2002 is now available. |
6 |
6 |
7 In this release many important aspects of Isabelle have been reworked |
7 In this release many important aspects of Isabelle have been reworked, |
8 to improve robustness and usability (this occasionally causes |
8 to improve robustness and usability. This occasionally causes |
9 incompatibility with earlier versions). |
9 incompatibility with earlier versions. |
10 |
10 |
11 The most prominent highlights of Isabelle2002 are as follows; see the |
11 The most prominent highlights of Isabelle2002 are as follows (see the |
12 NEWS of the distribution for more details. |
12 NEWS of the distribution for more details). |
13 |
13 |
14 * The Isabelle/HOL tutorial has been published as LNCS 2283; |
14 * The Isabelle/HOL tutorial has been published as LNCS 2283; |
15 Isabelle2002 is the official version to go along with that book. |
15 Isabelle2002 is the official version to go along with that book |
|
16 (by Tobias Nipkow, Larry Paulson, Markus Wenzel). |
16 |
17 |
17 * Explicit proof terms for Isabelle/Pure (Stefan Berghofer); |
18 * Pure: explicit proof terms for all internal inferences: |
18 all object-logics, proof tools etc. will automatically benefit. |
19 object-logics, proof tools etc. will benefit automatically |
|
20 (by Stefan Berghofer). |
19 |
21 |
20 * Interation of locales |
22 * Pure/Isar: proper integration of the locale package for modular |
|
23 theory development; additional support for rename/merge |
|
24 operations, and type-inference for structured specifications |
|
25 (by Markus Wenzel). |
21 |
26 |
22 * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2 |
27 * Pure/Isar: streamlined induction proof patterns |
23 (manage larger heaps, slightly faster). |
28 (by Markus Wenzel). |
24 |
29 |
|
30 * Pure/HOL: infrastructure for generating functional and relational |
|
31 code, using the ML run-time environment (by Stefan Berghofer). |
|
32 |
|
33 * HOL/library: sane numerals on all number types; several |
|
34 improvements of tuple and record types; new definite description |
|
35 operator; keep Hilbert's choice out of basic theories. |
|
36 |
|
37 * HOL/Bali: large application concerning formal treatment of Java. |
|
38 (by David von Oheimb and Norbert Schirmer). |
|
39 |
|
40 * HOL/Hoare_Parallel: large application concerning verification of |
|
41 parallel imperative programs (Owicki-Gries method etc.) |
|
42 (by Leonor Prensa Nieto). |
|
43 |
|
44 * HOL/GroupTheory: group theory examples including Sylow's theorem |
|
45 (by Florian Kammüller). |
|
46 |
|
47 * HOL/IMP: new proofs in Isar format |
|
48 (by Gerwin Klein). |
|
49 |
|
50 * ZF/UNITY: typeless version of Chandy and Misra's formalism |
|
51 (by Sidi O Ehmety). |
|
52 |
|
53 * System: improvements and simplifications of document preparation |
|
54 (by Markus Wenzel). |
|
55 |
|
56 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting |
|
57 larger heap size of applications. |
|
58 |
|
59 * System: support for MacOS X (for Poly/ML and SML/NJ). |
25 |
60 |
26 |
61 |
27 You may get Isabelle2002 from any of the following mirror sites: |
62 You may get Isabelle2002 from any of the following mirror sites: |
28 |
63 |
29 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
64 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |