ANNOUNCE
changeset 12983 7d13480ee668
parent 12964 2ac9265b2cd5
child 12993 1b76cc7ffef7
equal deleted inserted replaced
12982:34a07757634d 12983:7d13480ee668
     2 Subject: Announcing Isabelle2002
     2 Subject: Announcing Isabelle2002
     3 To: isabelle-users@cl.cam.ac.uk
     3 To: isabelle-users@cl.cam.ac.uk
     4 
     4 
     5 Isabelle2002 is now available.
     5 Isabelle2002 is now available.
     6 
     6 
     7 In this release many important aspects of Isabelle have been reworked
     7 In this release many important aspects of Isabelle have been reworked,
     8 to improve robustness and usability (this occasionally causes
     8 to improve robustness and usability.  This occasionally causes
     9 incompatibility with earlier versions).
     9 incompatibility with earlier versions.
    10 
    10 
    11 The most prominent highlights of Isabelle2002 are as follows; see the
    11 The most prominent highlights of Isabelle2002 are as follows (see the
    12 NEWS of the distribution for more details.
    12 NEWS of the distribution for more details).
    13 
    13 
    14   * The Isabelle/HOL tutorial has been published as LNCS 2283;
    14   * The Isabelle/HOL tutorial has been published as LNCS 2283;
    15     Isabelle2002 is the official version to go along with that book.
    15     Isabelle2002 is the official version to go along with that book
       
    16     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    16 
    17 
    17   * Explicit proof terms for Isabelle/Pure (Stefan Berghofer);
    18   * Pure: explicit proof terms for all internal inferences:
    18     all object-logics, proof tools etc. will automatically benefit.
    19     object-logics, proof tools etc. will benefit automatically
       
    20     (by Stefan Berghofer).
    19 
    21 
    20   * Interation of locales
    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).
    21 
    26 
    22   * Specific support for Poly/ML 4.1.1 and PolyML/4.1.2
    27   * Pure/Isar: streamlined induction proof patterns
    23     (manage larger heaps, slightly faster).
    28     (by Markus Wenzel).
    24 
    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).
    25 
    60 
    26 
    61 
    27 You may get Isabelle2002 from any of the following mirror sites:
    62 You may get Isabelle2002 from any of the following mirror sites:
    28 
    63 
    29   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    64   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/