ANNOUNCE
changeset 13042 d8a345d9e067
parent 13010 3437d8d89803
child 13045 1db0bdda1d32
equal deleted inserted replaced
13041:6faccf7d0f25 13042:d8a345d9e067
    16 
    16 
    17   * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    17   * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    18     Isabelle2002 is the official version to go along with that book
    18     Isabelle2002 is the official version to go along with that book
    19     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    19     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    20 
    20 
    21   * Pure: explicit proof terms for all internal inferences:
    21   * Pure: explicit proof terms for all internal inferences;
    22     object-logics, proof tools etc. will benefit automatically
    22     object-logics, proof tools etc. will benefit automatically
    23     (by Stefan Berghofer).
    23     (by Stefan Berghofer).
    24 
    24 
    25   * Pure/Isar: proper integration of the locale package for modular
    25   * Pure/Isar: proper integration of the locale package for modular
    26     theory development; additional support for rename/merge
    26     theory development; additional support for rename/merge
    27     operations, and type-inference for structured specifications
    27     operations, and type-inference for structured specifications
    28     (by Markus Wenzel).
    28     (by Markus Wenzel).
    29 
    29 
    30   * Pure/Isar: streamlined induction proof patterns
    30   * Pure/Isar: streamlined cases/induction proof patterns
    31     (by Markus Wenzel).
    31     (by Markus Wenzel).
    32 
    32 
    33   * Pure/HOL: infrastructure for generating functional and relational
    33   * Pure/HOL: infrastructure for generating functional and relational
    34     code, using the ML run-time environment (by Stefan Berghofer).
    34     code, using the ML run-time environment
       
    35     (by Stefan Berghofer).
    35 
    36 
    36   * HOL/library: numerals on all number types; several
    37   * HOL/library: numerals on all number types; several improvements of
    37     improvements of tuple and record types; new definite description
    38     tuple and record types; new definite description operator; keep
    38     operator; keep Hilbert's epsilon (Axiom of Choice) out of basic theories.
    39     Hilbert's epsilon (Axiom of Choice) out of basic theories
       
    40     (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
    39 
    41 
    40   * HOL/Bali: large application concerning formal treatment of Java.
    42   * HOL/Bali: large application concerning formal treatment of Java.
    41     (by David von Oheimb and Norbert Schirmer).
    43     (by David von Oheimb and Norbert Schirmer).
    42 
    44 
    43   * HOL/HoareParallel: large application concerning verification of
    45   * HOL/HoareParallel: large application concerning verification of
    44     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    46     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    45     method, examples of garbage collection, mutual exclusion, etc.)
    47     method, examples of garbage collection, mutual exclusion)
    46     (by Leonor Prensa Nieto).
    48     (by Leonor Prensa Nieto).
    47 
    49 
    48   * HOL/GroupTheory: group theory examples including Sylow's theorem
    50   * HOL/GroupTheory: group theory examples including Sylow's theorem
    49     (by Florian Kammüller).
    51     (by Florian Kammueller).
    50 
    52 
    51   * HOL/IMP: new proofs in Isar format
    53   * HOL/IMP: several new proofs in Isar format
    52     (by Gerwin Klein).
    54     (by Gerwin Klein).
    53 
    55 
    54   * HOL/MicroJava: exception handling on the bytecode level
    56   * HOL/MicroJava: exception handling on the bytecode level
    55     (by Gerwin Klein).
    57     (by Gerwin Klein).
    56 
    58 
    59 
    61 
    60   * System: improvements and simplifications of document preparation
    62   * System: improvements and simplifications of document preparation
    61     (by Markus Wenzel).
    63     (by Markus Wenzel).
    62 
    64 
    63   * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    65   * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    64     larger heap size of applications.
    66     larger heap size of applications; support for MacOS X (Poly/ML and
    65 
    67     SML/NJ).
    66   * System: support for MacOS X (for Poly/ML and SML/NJ).
       
    67 
       
    68 
    68 
    69 You may get Isabelle2002 from any of the following mirror sites:
    69 You may get Isabelle2002 from any of the following mirror sites:
    70 
    70 
    71   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    71   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    72   Munich (Germany)  http://isabelle.in.tum.de/dist/
    72   Munich (Germany)  http://isabelle.in.tum.de/dist/