ANNOUNCE
changeset 14614 196ff8d245bf
parent 14023 180f01d9df2c
child 14616 b167b1b848d8
equal deleted inserted replaced
14613:f0e4b502a208 14614:196ff8d245bf
     1 Subject: Announcing Isabelle2003
     1 Subject: Announcing Isabelle2004
     2 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     3 
     4 Isabelle2003 is now available.
     4 Isabelle2004 is now available.
     5 
     5 
     6 This release provides many improvements and a few substantial advances over
     6 This release provides many improvements and a few substantial advances over
     7 Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
     7 Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
     8 (see the NEWS of the distribution for more details):
     8 (see the NEWS of the distribution for more details):
     9 
     9 
    10  * New framework for extracting programs from constructive proofs in HOL.
       
    11    (Berghofer)
       
    12 
    10 
    13  * Improved simplifier. The premises of a goal are completely
    11 * New theory Ring_and_Field with over 250 basic numerical laws, 
    14    interreduced, ie simplified wrt each other. (Berghofer)
    12   all proved in axiomatic type classes for semirings, rings and fields.
    15 
    13 
    16  * Presburger arithmetic. Method arith can deal with quantified formulae over
    14 * Type "rat" of the rational numbers available in HOL-Complex.
    17    nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
       
    18 
    15 
    19  * New command to find all rules whose conclusion matches the current goal.
    16 * New locale "ring" for non-commutative rings in HOL-Algebra.
    20 
    17 
    21  * New command to trace why unification failed.
    18 * New theory of matrices with an application to linear programming in
       
    19   HOL-Matrix.
    22 
    20 
    23  * Locales (named proof contexts).  The new implementation is fully
    21 * Improved locales (named proof contexts), instantiation of locales.
    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 
    22 
    28  * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
    23 * Improved handling of linear and partial orders in simplifier.
    29    algebraic developments in HOL.  Currently covers group and ring theory.
    24  
    30    (Ballarin, Kammüller, Paulson)
    25 * New "specification" command for definition by specification.
    31 
    26 
    32  * HOL/Complex defines the type "complex" of the complex numbers, with numeric
    27 * New Isar command "finalconsts" prevents constants being given a definition
    33    constants and some complex analysis, including nonstandard analysis.  The
    28   later.
    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 
    29 
    38  * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
    30 * Command "arith" now generates counterexamples for reals as well.
    39    Gray and Kramer)
       
    40 
    31 
    41  * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
    32 * New "quickcheck" command to search for counterexamples of executable goals.
    42    of choice is mechanized using Isabelle/ZF, following Kunen's well-known
    33   (see HOL/ex/Quickcheck_Examples.thy)
    43    textbook "Set Theory". (Paulson)
    34 
       
    35 * New "refute" command to search for finite countermodels of goals.
       
    36   (see HOL/ex/Refute_Examples.thy)
       
    37 
       
    38 * Presentation and x-symbol enhancements, greek letters and sub/superscripts
       
    39   allowed in identifiers.
       
    40 
    44 
    41 
    45 You may get Isabelle2003 from the following mirror sites:
    42 You may get Isabelle2003 from the following mirror sites:
    46 
    43 
    47   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    44   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    48   Munich (Germany)  http://isabelle.in.tum.de/dist/
    45   Munich (Germany)  http://isabelle.in.tum.de/dist/