2 Subject: Announcing Isabelle2002
3 To: isabelle-users@cl.cam.ac.uk
5 Isabelle2002 is now available.
7 This release provides major improvements. The Isar language has
8 reached a mature state; the core engine is able to record full proof
9 terms; many aspects of the library have been reworked; several
10 substantial case studies have been added. Some changes may cause
11 incompatibility with earlier versions, but improve accessibility of
12 Isabelle for new users.
14 The most prominent highlights of Isabelle2002 are as follows (see the
15 NEWS of the distribution for more details).
17 * The Isabelle/HOL tutorial is to be published as LNCS 2283;
18 Isabelle2002 is the official version to go along with that book
19 (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
21 * Pure: explicit proof terms for all internal inferences:
22 object-logics, proof tools etc. will benefit automatically
23 (by Stefan Berghofer).
25 * Pure/Isar: proper integration of the locale package for modular
26 theory development; additional support for rename/merge
27 operations, and type-inference for structured specifications
30 * Pure/Isar: streamlined induction proof patterns
33 * Pure/HOL: infrastructure for generating functional and relational
34 code, using the ML run-time environment (by Stefan Berghofer).
36 * HOL/library: numerals on all number types; several
37 improvements of tuple and record types; new definite description
38 operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
40 * HOL/Bali: large application concerning formal treatment of Java.
41 (by David von Oheimb and Norbert Schirmer).
43 * HOL/HoareParallel: large application concerning verification of
44 parallel imperative programs (Owicki-Gries method, Rely-Guarantee
45 method, including examples of garbage collection, mutual
47 (by Leonor Prensa Nieto).
49 * HOL/GroupTheory: group theory examples including Sylow's theorem
50 (by Florian Kammüller).
52 * HOL/IMP: new proofs in Isar format
55 * ZF/UNITY: typeless version of Chandy and Misra's formalism
58 * System: improvements and simplifications of document preparation
61 * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
62 larger heap size of applications.
64 * System: support for MacOS X (for Poly/ML and SML/NJ).
67 You may get Isabelle2002 from any of the following mirror sites:
69 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
70 Munich (Germany) http://isabelle.in.tum.de/dist/
71 New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
72 Stanford (USA) ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html