# HG changeset patch
# User wenzelm
# Date 1275903762 -7200
# Node ID b6222a65bacf97d39fe3719e3652ed141238b20d
# Parent  c4f393759c5931b9e9f422a3ec8db08a6fb5ce8a
tuned ANNOUNCEMENT;

diff -r c4f393759c59 -r b6222a65bacf ANNOUNCE
--- a/ANNOUNCE	Mon Jun 07 11:42:32 2010 +0200
+++ b/ANNOUNCE	Mon Jun 07 11:42:42 2010 +0200
@@ -9,23 +9,24 @@
 
 * 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.
+* Robust treatment of concrete syntax for different logical entities;
+mixfix syntax in local proof context.
 
-* HOL: Package for constructing quotient types.
+* Type declarations and notation within local theory context.
+
+* HOL: package for 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 code generation: simple concept for abstract datatypes obeying
+invariants (e.g. red-black trees).
 
-* HOL: New development of the Reals using Cauchy Sequences.
+* HOL: new development of the Reals using Cauchy Sequences.
 
-* HOL: Reorganization of abstract algebra type class hierarchy.
+* 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.
+* HOL: substantial reorganization of main library and related tools.
+
+* HOLCF: reorganization of 'domain' package.
+
 
 You may get Isabelle2009-2 from the following mirror sites: