ANNOUNCE
author nipkow
Mon May 12 19:54:43 2003 +0200 (2003-05-12)
changeset 14023 180f01d9df2c
parent 14022 3407f1b807ce
child 14614 196ff8d245bf
permissions -rw-r--r--
*** empty log message ***
     1 Subject: Announcing Isabelle2003
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2003 is now available.
     5 
     6 This release provides many improvements and a few substantial advances over
     7 Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
     8 (see the NEWS of the distribution for more details):
     9 
    10  * New framework for extracting programs from constructive proofs in HOL.
    11    (Berghofer)
    12 
    13  * Improved simplifier. The premises of a goal are completely
    14    interreduced, ie simplified wrt each other. (Berghofer)
    15 
    16  * Presburger arithmetic. Method arith can deal with quantified formulae over
    17    nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
    18 
    19  * New command to find all rules whose conclusion matches the current goal.
    20 
    21  * New command to trace why unification failed.
    22 
    23  * Locales (named proof contexts).  The new implementation is fully
    24    integrated with Isar's notion of proof context, and locale specifications
    25    produce predicate definitions that allow to work with locales in more
    26    flexible ways. (Wenzel)
    27 
    28  * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
    29    algebraic developments in HOL.  Currently covers group and ring theory.
    30    (Ballarin, Kammüller, Paulson)
    31 
    32  * HOL/Complex defines the type "complex" of the complex numbers, with numeric
    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)
    37 
    38  * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
    39    Gray and Kramer)
    40 
    41  * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
    42    of choice is mechanized using Isabelle/ZF, following Kunen's well-known
    43    textbook "Set Theory". (Paulson)
    44 
    45 You may get Isabelle2003 from the following mirror sites:
    46 
    47   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    48   Munich (Germany)  http://isabelle.in.tum.de/dist/
    49 
    50 Gerwin Klein
    51 Tobias Nipkow
    52 Larry Paulson