ANNOUNCE
author blanchet
Tue Oct 05 11:45:10 2010 +0200 (2010-10-05)
changeset 39953 aa54f347e5e2
parent 37353 b6222a65bacf
child 41604 313b0033034a
permissions -rw-r--r--
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
     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/