author haftmann
Fri, 04 Jun 2010 16:42:26 +0200
changeset 37317 5164c4ec787b
parent 37159 07f3f5a03e98
child 37353 b6222a65bacf
permissions -rw-r--r--
first proposal for a announcement

Subject: Announcing Isabelle2009-2

Isabelle2009-2 is now available.

This release improves upon Isabelle2009-1 in many respects, see the
NEWS file in the distribution for more details.  Some notable changes

* Explicit proof terms for type class reasoning.

* Authentic syntax for *all* logical entities (type classes, type
constructors, term constants): provides simple and robust
correspondence between formal entities and concrete syntax.

* HOL: Package for constructing quotient types.

* HOL: Code generation now with simple concept for abstract
datatypes obeying invariants;  applications for typical data structures
(e.g. search trees) can be found in the library.

* HOL: New development of the Reals using Cauchy Sequences.

* HOL: Reorganization of abstract algebra type class hierarchy.

* Commands 'types', 'typedecl' and 'typedef' now work within a local theory
context -- without introducing dependencies on parameters or

You may get Isabelle2009-2 from the following mirror sites:

  Cambridge (UK)
  Munich (Germany)
  Sydney (Australia)