ANNOUNCE
changeset 14021 24bf519625ab
parent 13045 1db0bdda1d32
child 14022 3407f1b807ce
equal deleted inserted replaced
14020:5fc9474833e5 14021:24bf519625ab
     1 
     1 Subject: Announcing Isabelle2003
     2 Subject: Announcing Isabelle2002
       
     3 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     4 
     3 
     5 Isabelle2002 is now available.
     4 Isabelle2003 is now available.
     6 
     5 
     7 This release provides major improvements.  The Isar language has
     6 This release provides many improvements and a few substantial advances over
     8 reached a mature state; the core engine is able to record full proof
     7 Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
     9 terms; many aspects of the library have been reworked; several
     8 (see the NEWS of the distribution for more details):
    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 
     9 
    14 The most prominent highlights of Isabelle2002 are as follows (see the
    10  * New framework for extracting programs from constructive proofs in HOL.
    15 NEWS of the distribution for more details).
    11    (Berghofer)
    16 
    12 
    17   * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    13  * Improved simplifier. The premises of a goal are completely
    18     Isabelle2002 is the official version to go along with that book
    14    interreduced, ie simplified wrt each other. (Berghofer)
    19     (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
       
    20 
    15 
    21   * Pure: explicit proof terms for all internal inferences;
    16  * Presburger arithmetic. Method arith can deal with quantified formulae over
    22     object-logics, proof tools etc. will benefit automatically
    17    nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
    23     (by Stefan Berghofer).
       
    24 
    18 
    25   * Pure/Isar: proper integration of the locale package for modular
    19  * New command to find all rules whose conclusion matches the current goal.
    26     theory development; additional support for rename/merge
       
    27     operations, and type-inference for structured specifications
       
    28     (by Markus Wenzel).
       
    29 
    20 
    30   * Pure/Isar: streamlined cases/induction proof patterns
    21  * New command to trace why unification failed.
    31     (by Markus Wenzel).
       
    32 
    22 
    33   * Pure/HOL: infrastructure for generating functional and relational
    23  * Locales (named proof contexts).  The new implementation is fully
    34     code, using the ML run-time environment
    24    integrated with Isar's notion of proof context, and locale specifications
    35     (by Stefan Berghofer).
    25    produce predicate definitions that allow to work with locales in more
       
    26    flexible ways. (Wenzel)
    36 
    27 
    37   * HOL/library: numerals on all number types; several improvements of
    28  * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
    38     tuple and record types; new definite description operator; keep
    29    algebraic developments in HOL.  Currently covers group and ring theory.
    39     Hilbert's epsilon (Axiom of Choice) out of basic theories
    30    (Ballarin, Kammüller, Paulson)
    40     (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
       
    41 
    31 
    42   * HOL/Bali: large application concerning formal treatment of Java.
    32  * HOL/Complex defines the type "complex" of the complex numbers, with numeric
    43     (by David von Oheimb and Norbert Schirmer).
    33    constants and some complex analysis, including nonstandard analysis.  The
       
    34    image HOL-Complex should be used for developments involving the real
       
    35    numbers too.  Gauge integration and hyperreal logarithms have recently
       
    36    been added. (Fleuriot)
    44 
    37 
    45   * HOL/HoareParallel: large application concerning verification of
    38  * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
    46     parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    39    Gray and Kramer)
    47     method, examples of garbage collection, mutual exclusion)
       
    48     (by Leonor Prensa Nieto).
       
    49 
    40 
    50   * HOL/GroupTheory: group theory examples including Sylow's theorem
    41  * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
    51     (by Florian Kammueller).
    42    of choice is mechanized using Isabelle/ZF, following, Kunen's famous
       
    43    textbook "Set Theory". (Paulson)
    52 
    44 
    53   * HOL/IMP: several new proofs in Isar format
    45 You may get Isabelle2003 from any of the following mirror sites:
    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 
    46 
    71   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    47   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    72   Munich (Germany)  http://isabelle.in.tum.de/dist/
    48   Munich (Germany)  http://isabelle.in.tum.de/dist/
    73   New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html