diff -r f0e4b502a208 -r 196ff8d245bf ANNOUNCE
--- 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: