2003 -> 2004
authornipkow
Sat Apr 17 14:51:00 2004 +0200 (2004-04-17)
changeset 14614196ff8d245bf
parent 14613 f0e4b502a208
child 14615 603f08285c65
2003 -> 2004
ANNOUNCE
     1.1 --- a/ANNOUNCE	Sat Apr 17 13:56:59 2004 +0200
     1.2 +++ b/ANNOUNCE	Sat Apr 17 14:51:00 2004 +0200
     1.3 @@ -1,46 +1,43 @@
     1.4 -Subject: Announcing Isabelle2003
     1.5 +Subject: Announcing Isabelle2004
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2003 is now available.
     1.9 +Isabelle2004 is now available.
    1.10  
    1.11  This release provides many improvements and a few substantial advances over
    1.12 -Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
    1.13 +Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
    1.14  (see the NEWS of the distribution for more details):
    1.15  
    1.16 - * New framework for extracting programs from constructive proofs in HOL.
    1.17 -   (Berghofer)
    1.18  
    1.19 - * Improved simplifier. The premises of a goal are completely
    1.20 -   interreduced, ie simplified wrt each other. (Berghofer)
    1.21 +* New theory Ring_and_Field with over 250 basic numerical laws, 
    1.22 +  all proved in axiomatic type classes for semirings, rings and fields.
    1.23 +
    1.24 +* Type "rat" of the rational numbers available in HOL-Complex.
    1.25  
    1.26 - * Presburger arithmetic. Method arith can deal with quantified formulae over
    1.27 -   nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
    1.28 +* New locale "ring" for non-commutative rings in HOL-Algebra.
    1.29  
    1.30 - * New command to find all rules whose conclusion matches the current goal.
    1.31 +* New theory of matrices with an application to linear programming in
    1.32 +  HOL-Matrix.
    1.33  
    1.34 - * New command to trace why unification failed.
    1.35 +* Improved locales (named proof contexts), instantiation of locales.
    1.36  
    1.37 - * Locales (named proof contexts).  The new implementation is fully
    1.38 -   integrated with Isar's notion of proof context, and locale specifications
    1.39 -   produce predicate definitions that allow to work with locales in more
    1.40 -   flexible ways. (Wenzel)
    1.41 +* Improved handling of linear and partial orders in simplifier.
    1.42 + 
    1.43 +* New "specification" command for definition by specification.
    1.44  
    1.45 - * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
    1.46 -   algebraic developments in HOL.  Currently covers group and ring theory.
    1.47 -   (Ballarin, Kammüller, Paulson)
    1.48 +* New Isar command "finalconsts" prevents constants being given a definition
    1.49 +  later.
    1.50 +
    1.51 +* Command "arith" now generates counterexamples for reals as well.
    1.52  
    1.53 - * HOL/Complex defines the type "complex" of the complex numbers, with numeric
    1.54 -   constants and some complex analysis, including nonstandard analysis.  The
    1.55 -   image HOL-Complex should be used for developments involving the real
    1.56 -   numbers too.  Gauge integration and hyperreal logarithms have recently
    1.57 -   been added. (Fleuriot)
    1.58 +* New "quickcheck" command to search for counterexamples of executable goals.
    1.59 +  (see HOL/ex/Quickcheck_Examples.thy)
    1.60  
    1.61 - * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
    1.62 -   Gray and Kramer)
    1.63 +* New "refute" command to search for finite countermodels of goals.
    1.64 +  (see HOL/ex/Refute_Examples.thy)
    1.65  
    1.66 - * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
    1.67 -   of choice is mechanized using Isabelle/ZF, following Kunen's well-known
    1.68 -   textbook "Set Theory". (Paulson)
    1.69 +* Presentation and x-symbol enhancements, greek letters and sub/superscripts
    1.70 +  allowed in identifiers.
    1.71 +
    1.72  
    1.73  You may get Isabelle2003 from the following mirror sites:
    1.74