# HG changeset patch
# User blanchet
# Date 1275663325 -7200
# Node ID 81f058f2d2ff46f36e98527be70642b6c0821922
# Parent  51d99ba6fc4d52cc0d1383bb79a0f438ee3ee246# Parent  5164c4ec787b228586866a78e38b4b6c0286396e
merge

diff -r 51d99ba6fc4d -r 81f058f2d2ff ANNOUNCE
--- a/ANNOUNCE	Fri Jun 04 16:55:08 2010 +0200
+++ b/ANNOUNCE	Fri Jun 04 16:55:25 2010 +0200
@@ -7,8 +7,25 @@
 NEWS file in the distribution for more details.  Some notable changes
 are:
 
-* FIXME
+* Explicit proof terms for type class reasoning.
+
+* Authentic syntax for *all* logical entities (type classes, type
+constructors, term constants): provides simple and robust
+correspondence between formal entities and concrete syntax.
+
+* HOL: Package for constructing quotient types.
 
+* HOL: Code generation now with simple concept for abstract
+datatypes obeying invariants;  applications for typical data structures
+(e.g. search trees) can be found in the library.
+
+* HOL: New development of the Reals using Cauchy Sequences.
+
+* HOL: Reorganization of abstract algebra type class hierarchy.
+
+* Commands 'types', 'typedecl' and 'typedef' now work within a local theory
+context -- without introducing dependencies on parameters or
+assumptions.
 
 You may get Isabelle2009-2 from the following mirror sites:
 
diff -r 51d99ba6fc4d -r 81f058f2d2ff NEWS
--- a/NEWS	Fri Jun 04 16:55:08 2010 +0200
+++ b/NEWS	Fri Jun 04 16:55:25 2010 +0200
@@ -139,6 +139,10 @@
 * Command 'defaultsort' has been renamed to 'default_sort', it works
 within a local theory context.  Minor INCOMPATIBILITY.
 
+* Raw axioms/defs may no longer carry sort constraints, and raw defs
+may no longer carry premises. User-level specifications are
+transformed accordingly by Thm.add_axiom/add_def.
+
 * Proof terms: Type substitutions on proof constants now use canonical
 order of type variables.  INCOMPATIBILITY for tools working with proof
 terms.