author | nipkow |

Sat Apr 17 14:51:00 2004 +0200 (2004-04-17) | |

changeset 14614 | 196ff8d245bf |

parent 14613 | f0e4b502a208 |

child 14615 | 603f08285c65 |

2003 -> 2004

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