ANNOUNCE
author haftmann
Fri Aug 20 17:46:55 2010 +0200 (2010-08-20)
changeset 38620 b40524b74f77
parent 37353 b6222a65bacf
child 41604 313b0033034a
permissions -rw-r--r--
inj_comp and inj_fun
wenzelm@37159
     1
Subject: Announcing Isabelle2009-2
wenzelm@9928
     2
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     3
wenzelm@37159
     4
Isabelle2009-2 is now available.
wenzelm@17544
     5
wenzelm@37159
     6
This release improves upon Isabelle2009-1 in many respects, see the
wenzelm@37159
     7
NEWS file in the distribution for more details.  Some notable changes
wenzelm@30848
     8
are:
wenzelm@27007
     9
haftmann@37317
    10
* Explicit proof terms for type class reasoning.
haftmann@37317
    11
wenzelm@37353
    12
* Robust treatment of concrete syntax for different logical entities;
wenzelm@37353
    13
mixfix syntax in local proof context.
haftmann@37317
    14
wenzelm@37353
    15
* Type declarations and notation within local theory context.
wenzelm@37353
    16
wenzelm@37353
    17
* HOL: package for quotient types.
wenzelm@33873
    18
wenzelm@37353
    19
* HOL code generation: simple concept for abstract datatypes obeying
wenzelm@37353
    20
invariants (e.g. red-black trees).
haftmann@37317
    21
wenzelm@37353
    22
* HOL: new development of the Reals using Cauchy Sequences.
haftmann@37317
    23
wenzelm@37353
    24
* HOL: reorganization of abstract algebra type class hierarchy.
haftmann@37317
    25
wenzelm@37353
    26
* HOL: substantial reorganization of main library and related tools.
wenzelm@37353
    27
wenzelm@37353
    28
* HOLCF: reorganization of 'domain' package.
wenzelm@37353
    29
wenzelm@12983
    30
wenzelm@37159
    31
You may get Isabelle2009-2 from the following mirror sites:
wenzelm@9928
    32
haftmann@27085
    33
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
haftmann@17696
    34
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    35
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/