ANNOUNCE
changeset 37317 5164c4ec787b
parent 37159 07f3f5a03e98
child 37353 b6222a65bacf
equal deleted inserted replaced
37316:52dc576f1759 37317:5164c4ec787b
     5 
     5 
     6 This release improves upon Isabelle2009-1 in many respects, see the
     6 This release improves upon Isabelle2009-1 in many respects, see the
     7 NEWS file in the distribution for more details.  Some notable changes
     7 NEWS file in the distribution for more details.  Some notable changes
     8 are:
     8 are:
     9 
     9 
    10 * FIXME
    10 * Explicit proof terms for type class reasoning.
    11 
    11 
       
    12 * Authentic syntax for *all* logical entities (type classes, type
       
    13 constructors, term constants): provides simple and robust
       
    14 correspondence between formal entities and concrete syntax.
       
    15 
       
    16 * HOL: Package for constructing quotient types.
       
    17 
       
    18 * HOL: Code generation now with simple concept for abstract
       
    19 datatypes obeying invariants;  applications for typical data structures
       
    20 (e.g. search trees) can be found in the library.
       
    21 
       
    22 * HOL: New development of the Reals using Cauchy Sequences.
       
    23 
       
    24 * HOL: Reorganization of abstract algebra type class hierarchy.
       
    25 
       
    26 * Commands 'types', 'typedecl' and 'typedef' now work within a local theory
       
    27 context -- without introducing dependencies on parameters or
       
    28 assumptions.
    12 
    29 
    13 You may get Isabelle2009-2 from the following mirror sites:
    30 You may get Isabelle2009-2 from the following mirror sites:
    14 
    31 
    15   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    32   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    16   Munich (Germany)     http://isabelle.in.tum.de/
    33   Munich (Germany)     http://isabelle.in.tum.de/