ANNOUNCE
author haftmann
Fri Jun 04 16:42:26 2010 +0200 (2010-06-04)
changeset 37317 5164c4ec787b
parent 37159 07f3f5a03e98
child 37353 b6222a65bacf
permissions -rw-r--r--
first proposal for a announcement
     1 Subject: Announcing Isabelle2009-2
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2009-2 is now available.
     5 
     6 This release improves upon Isabelle2009-1 in many respects, see the
     7 NEWS file in the distribution for more details.  Some notable changes
     8 are:
     9 
    10 * Explicit proof terms for type class reasoning.
    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.
    29 
    30 You may get Isabelle2009-2 from the following mirror sites:
    31 
    32   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    33   Munich (Germany)     http://isabelle.in.tum.de/
    34   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/