Mon, 07 Jun 2010 11:42:42 +0200
changeset 37353 b6222a65bacf
parent 37352 c4f393759c59
child 37354 865ad5634ed8
--- 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
+* HOL: substantial reorganization of main library and related tools.
+* HOLCF: reorganization of 'domain' package.
 You may get Isabelle2009-2 from the following mirror sites: