ANNOUNCE
author wenzelm
Thu Mar 07 23:21:19 2002 +0100 (2002-03-07)
changeset 13042 d8a345d9e067
parent 13010 3437d8d89803
child 13045 1db0bdda1d32
permissions -rw-r--r--
tuned;
     1 
     2 Subject: Announcing Isabelle2002
     3 To: isabelle-users@cl.cam.ac.uk
     4 
     5 Isabelle2002 is now available.
     6 
     7 This release provides major improvements.  The Isar language has
     8 reached a mature state; the core engine is able to record full proof
     9 terms; many aspects of the library have been reworked; several
    10 substantial case studies have been added.  Some changes may cause
    11 incompatibility with earlier versions, but improve accessibility of
    12 Isabelle for new users.
    13 
    14 The most prominent highlights of Isabelle2002 are as follows (see the
    15 NEWS of the distribution for more details).
    16 
    17   * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    18     Isabelle2002 is the official version to go along with that book
    19     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    20 
    21   * Pure: explicit proof terms for all internal inferences;
    22     object-logics, proof tools etc. will benefit automatically
    23     (by Stefan Berghofer).
    24 
    25   * Pure/Isar: proper integration of the locale package for modular
    26     theory development; additional support for rename/merge
    27     operations, and type-inference for structured specifications
    28     (by Markus Wenzel).
    29 
    30   * Pure/Isar: streamlined cases/induction proof patterns
    31     (by Markus Wenzel).
    32 
    33   * Pure/HOL: infrastructure for generating functional and relational
    34     code, using the ML run-time environment
    35     (by Stefan Berghofer).
    36 
    37   * HOL/library: numerals on all number types; several improvements of
    38     tuple and record types; new definite description operator; keep
    39     Hilbert's epsilon (Axiom of Choice) out of basic theories
    40     (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
    41 
    42   * HOL/Bali: large application concerning formal treatment of Java.
    43     (by David von Oheimb and Norbert Schirmer).
    44 
    45   * HOL/HoareParallel: large application concerning verification of
    46     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    47     method, examples of garbage collection, mutual exclusion)
    48     (by Leonor Prensa Nieto).
    49 
    50   * HOL/GroupTheory: group theory examples including Sylow's theorem
    51     (by Florian Kammueller).
    52 
    53   * HOL/IMP: several new proofs in Isar format
    54     (by Gerwin Klein).
    55 
    56   * HOL/MicroJava: exception handling on the bytecode level
    57     (by Gerwin Klein).
    58 
    59   * ZF/UNITY: typeless version of Chandy and Misra's formalism
    60     (by Sidi O Ehmety).
    61 
    62   * System: improvements and simplifications of document preparation
    63     (by Markus Wenzel).
    64 
    65   * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    66     larger heap size of applications; support for MacOS X (Poly/ML and
    67     SML/NJ).
    68 
    69 You may get Isabelle2002 from any of the following mirror sites:
    70 
    71   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    72   Munich (Germany)  http://isabelle.in.tum.de/dist/
    73   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html
    74   Stanford (USA)    ftp://rodin.stanford.edu/pub/smlnj/isabelle/index.html