--- 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: