ANNOUNCE
author wenzelm
Thu Feb 28 21:30:03 2002 +0100 (2002-02-28)
changeset 12983 7d13480ee668
parent 12964 2ac9265b2cd5
child 12993 1b76cc7ffef7
permissions -rw-r--r--
more stuff;
     1 
     2 Subject: Announcing Isabelle2002
     3 To: isabelle-users@cl.cam.ac.uk
     4 
     5 Isabelle2002 is now available.
     6 
     7 In this release many important aspects of Isabelle have been reworked,
     8 to improve robustness and usability.  This occasionally causes
     9 incompatibility with earlier versions.
    10 
    11 The most prominent highlights of Isabelle2002 are as follows (see the
    12 NEWS of the distribution for more details).
    13 
    14   * The Isabelle/HOL tutorial has been published as LNCS 2283;
    15     Isabelle2002 is the official version to go along with that book
    16     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    17 
    18   * Pure: explicit proof terms for all internal inferences:
    19     object-logics, proof tools etc. will benefit automatically
    20     (by Stefan Berghofer).
    21 
    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).
    26 
    27   * Pure/Isar: streamlined induction proof patterns
    28     (by Markus Wenzel).
    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).
    60 
    61 
    62 You may get Isabelle2002 from any of the following mirror sites:
    63 
    64   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    65   Munich (Germany)  http://isabelle.in.tum.de/dist/
    66   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    67   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html