author wenzelm
Thu, 28 Feb 2002 21:30:03 +0100
changeset 12983 7d13480ee668
parent 12964 2ac9265b2cd5
child 12993 1b76cc7ffef7
permissions -rw-r--r--
more stuff;

Subject: Announcing Isabelle2002

Isabelle2002 is now available.

In this release many important aspects of Isabelle have been reworked,
to improve robustness and usability.  This occasionally causes
incompatibility with earlier versions.

The most prominent highlights of Isabelle2002 are as follows (see the
NEWS of the distribution for more details).

  * The Isabelle/HOL tutorial has been 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 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: sane numerals on all number types; several
    improvements of tuple and record types; new definite description
    operator; keep Hilbert's choice out of basic theories.

  * HOL/Bali: large application concerning formal treatment of Java.
    (by David von Oheimb and Norbert Schirmer).

  * HOL/Hoare_Parallel: large application concerning verification of
    parallel imperative programs (Owicki-Gries method etc.)
    (by Leonor Prensa Nieto).

  * HOL/GroupTheory: group theory examples including Sylow's theorem
    (by Florian Kammüller).

  * HOL/IMP: new proofs in Isar format
    (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.

  * System: support for MacOS X (for Poly/ML and SML/NJ).

You may get Isabelle2002 from any of the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  New Jersey (USA)
  Stanford (USA)