tuned ANNOUNCEMENT;
authorwenzelm
Mon Jun 07 11:42:42 2010 +0200 (2010-06-07)
changeset 37353b6222a65bacf
parent 37352 c4f393759c59
child 37354 865ad5634ed8
tuned ANNOUNCEMENT;
ANNOUNCE
     1.1 --- a/ANNOUNCE	Mon Jun 07 11:42:32 2010 +0200
     1.2 +++ b/ANNOUNCE	Mon Jun 07 11:42:42 2010 +0200
     1.3 @@ -9,23 +9,24 @@
     1.4  
     1.5  * Explicit proof terms for type class reasoning.
     1.6  
     1.7 -* Authentic syntax for *all* logical entities (type classes, type
     1.8 -constructors, term constants): provides simple and robust
     1.9 -correspondence between formal entities and concrete syntax.
    1.10 +* Robust treatment of concrete syntax for different logical entities;
    1.11 +mixfix syntax in local proof context.
    1.12  
    1.13 -* HOL: Package for constructing quotient types.
    1.14 +* Type declarations and notation within local theory context.
    1.15 +
    1.16 +* HOL: package for quotient types.
    1.17  
    1.18 -* HOL: Code generation now with simple concept for abstract
    1.19 -datatypes obeying invariants;  applications for typical data structures
    1.20 -(e.g. search trees) can be found in the library.
    1.21 +* HOL code generation: simple concept for abstract datatypes obeying
    1.22 +invariants (e.g. red-black trees).
    1.23  
    1.24 -* HOL: New development of the Reals using Cauchy Sequences.
    1.25 +* HOL: new development of the Reals using Cauchy Sequences.
    1.26  
    1.27 -* HOL: Reorganization of abstract algebra type class hierarchy.
    1.28 +* HOL: reorganization of abstract algebra type class hierarchy.
    1.29  
    1.30 -* Commands 'types', 'typedecl' and 'typedef' now work within a local theory
    1.31 -context -- without introducing dependencies on parameters or
    1.32 -assumptions.
    1.33 +* HOL: substantial reorganization of main library and related tools.
    1.34 +
    1.35 +* HOLCF: reorganization of 'domain' package.
    1.36 +
    1.37  
    1.38  You may get Isabelle2009-2 from the following mirror sites:
    1.39