ANNOUNCE

Removed (now unneeded) declaration of realizers for induction on natural numbers.

+
−
+
−Subject: Announcing Isabelle2002
+
−To: [e-mail]
+
−
+
−Isabelle2002 is now available.
+
−
+
−This release provides major improvements.  The Isar language has
+
−reached a mature state; the core engine is able to record full proof
+
−terms; many aspects of the library have been reworked; several
+
−substantial case studies have been added.  Some changes may cause
+
−incompatibility with earlier versions, but improve accessibility of
+
−Isabelle for new users.
+
−
+
−The most prominent highlights of Isabelle2002 are as follows (see the
+
−NEWS of the distribution for more details).
+
−
+
−  * The Isabelle/HOL tutorial is to be published as LNCS 2283;
+
−    Isabelle2002 is the official version to go along with that book
+
−    (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
+
−
+
−  * Pure: explicit proof terms for all internal inferences;
+
−    object-logics, proof tools etc. will benefit automatically
+
−    (by Stefan Berghofer).
+
−
+
−  * Pure/Isar: proper integration of the locale package for modular
+
−    theory development; additional support for rename/merge
+
−    operations, and type-inference for structured specifications
+
−    (by Markus Wenzel).
+
−
+
−  * Pure/Isar: streamlined cases/induction proof patterns
+
−    (by Markus Wenzel).
+
−
+
−  * Pure/HOL: infrastructure for generating functional and relational
+
−    code, using the ML run-time environment
+
−    (by Stefan Berghofer).
+
−
+
−  * HOL/library: numerals on all number types; several improvements of
+
−    tuple and record types; new definite description operator; keep
+
−    Hilbert's epsilon (Axiom of Choice) out of basic theories
+
−    (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
+
−
+
−  * HOL/Bali: large application concerning formal treatment of Java.
+
−    (by David von Oheimb and Norbert Schirmer).
+
−
+
−  * HOL/HoareParallel: large application concerning verification of
+
−    parallel imperative programs (Owicki-Gries method, Rely-Guarantee
+
−    method, examples of garbage collection, mutual exclusion)
+
−    (by Leonor Prensa Nieto).
+
−
+
−  * HOL/GroupTheory: group theory examples including Sylow's theorem
+
−    (by Florian Kammueller).
+
−
+
−  * HOL/IMP: several new proofs in Isar format
+
−    (by Gerwin Klein).
+
−
+
−  * HOL/MicroJava: exception handling on the bytecode level
+
−    (by Gerwin Klein).
+
−
+
−  * ZF/UNITY: typeless version of Chandy and Misra's formalism
+
−    (by Sidi O Ehmety).
+
−
+
−  * System: improvements and simplifications of document preparation
+
−    (by Markus Wenzel).
+
−
+
−  * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
+
−    larger heap size of applications; support for MacOS X (Poly/ML and
+
−    SML/NJ).
+
−
+
−You may get Isabelle2002 from any of the following mirror sites:
+
−
+
−  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
+
−  Munich (Germany)  http://isabelle.in.tum.de/dist/
+
−  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html