summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

ANNOUNCE

changeset 14614 | 196ff8d245bf |

parent 14023 | 180f01d9df2c |

child 14616 | b167b1b848d8 |

--- a/ANNOUNCE Sat Apr 17 13:56:59 2004 +0200 +++ b/ANNOUNCE Sat Apr 17 14:51:00 2004 +0200 @@ -1,46 +1,43 @@ -Subject: Announcing Isabelle2003 +Subject: Announcing Isabelle2004 To: isabelle-users@cl.cam.ac.uk -Isabelle2003 is now available. +Isabelle2004 is now available. This release provides many improvements and a few substantial advances over -Isabelle2002. The most prominent highlights of Isabelle2003 are as follows +Isabelle2003. The most prominent highlights of Isabelle2004 are as follows (see the NEWS of the distribution for more details): - * New framework for extracting programs from constructive proofs in HOL. - (Berghofer) - * Improved simplifier. The premises of a goal are completely - interreduced, ie simplified wrt each other. (Berghofer) +* New theory Ring_and_Field with over 250 basic numerical laws, + all proved in axiomatic type classes for semirings, rings and fields. + +* Type "rat" of the rational numbers available in HOL-Complex. - * Presburger arithmetic. Method arith can deal with quantified formulae over - nat and int, and with mod, div and dvd wrt a numeral. (Chaieb and Nipkow) +* New locale "ring" for non-commutative rings in HOL-Algebra. - * New command to find all rules whose conclusion matches the current goal. +* New theory of matrices with an application to linear programming in + HOL-Matrix. - * New command to trace why unification failed. +* Improved locales (named proof contexts), instantiation of locales. - * Locales (named proof contexts). The new implementation is fully - integrated with Isar's notion of proof context, and locale specifications - produce predicate definitions that allow to work with locales in more - flexible ways. (Wenzel) +* Improved handling of linear and partial orders in simplifier. + +* New "specification" command for definition by specification. - * HOL/Algebra: proofs in classical algebra. Intended as a base for all - algebraic developments in HOL. Currently covers group and ring theory. - (Ballarin, Kammüller, Paulson) +* New Isar command "finalconsts" prevents constants being given a definition + later. + +* Command "arith" now generates counterexamples for reals as well. - * HOL/Complex defines the type "complex" of the complex numbers, with numeric - constants and some complex analysis, including nonstandard analysis. The - image HOL-Complex should be used for developments involving the real - numbers too. Gauge integration and hyperreal logarithms have recently - been added. (Fleuriot) +* New "quickcheck" command to search for counterexamples of executable goals. + (see HOL/ex/Quickcheck_Examples.thy) - * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad, - Gray and Kramer) +* New "refute" command to search for finite countermodels of goals. + (see HOL/ex/Refute_Examples.thy) - * ZF/Constructible: Gödel's proof of the relative consistency of the axiom - of choice is mechanized using Isabelle/ZF, following Kunen's well-known - textbook "Set Theory". (Paulson) +* Presentation and x-symbol enhancements, greek letters and sub/superscripts + allowed in identifiers. + You may get Isabelle2003 from the following mirror sites: