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
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
haftmann@37317
    12
* Authentic syntax for *all* logical entities (type classes, type
haftmann@37317
    13
constructors, term constants): provides simple and robust
haftmann@37317
    14
correspondence between formal entities and concrete syntax.
haftmann@37317
    15
haftmann@37317
    16
* HOL: Package for constructing quotient types.
wenzelm@33873
    17
haftmann@37317
    18
* HOL: Code generation now with simple concept for abstract
haftmann@37317
    19
datatypes obeying invariants;  applications for typical data structures
haftmann@37317
    20
(e.g. search trees) can be found in the library.
haftmann@37317
    21
haftmann@37317
    22
* HOL: New development of the Reals using Cauchy Sequences.
haftmann@37317
    23
haftmann@37317
    24
* HOL: Reorganization of abstract algebra type class hierarchy.
haftmann@37317
    25
haftmann@37317
    26
* Commands 'types', 'typedecl' and 'typedef' now work within a local theory
haftmann@37317
    27
context -- without introducing dependencies on parameters or
haftmann@37317
    28
assumptions.
wenzelm@12983
    29
wenzelm@37159
    30
You may get Isabelle2009-2 from the following mirror sites:
wenzelm@9928
    31
haftmann@27085
    32
  Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
haftmann@17696
    33
  Munich (Germany)     http://isabelle.in.tum.de/
kleing@14616
    34
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/