ANNOUNCE
author nipkow
Sun Oct 10 16:34:20 2010 +0200 (2010-10-10)
changeset 39976 2474347538b8
parent 37353 b6222a65bacf
child 41604 313b0033034a
permissions -rw-r--r--
simplified proof
     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 * Robust treatment of concrete syntax for different logical entities;
    13 mixfix syntax in local proof context.
    14 
    15 * Type declarations and notation within local theory context.
    16 
    17 * HOL: package for quotient types.
    18 
    19 * HOL code generation: simple concept for abstract datatypes obeying
    20 invariants (e.g. red-black trees).
    21 
    22 * HOL: new development of the Reals using Cauchy Sequences.
    23 
    24 * HOL: reorganization of abstract algebra type class hierarchy.
    25 
    26 * HOL: substantial reorganization of main library and related tools.
    27 
    28 * HOLCF: reorganization of 'domain' package.
    29 
    30 
    31 You may get Isabelle2009-2 from the following mirror sites:
    32 
    33   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    34   Munich (Germany)     http://isabelle.in.tum.de/
    35   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/