ANNOUNCE

"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.

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