ANNOUNCE
changeset 41604 313b0033034a
parent 37353 b6222a65bacf
child 41605 7d035da21e9c
equal deleted inserted replaced
41603:54a4512e29a6 41604:313b0033034a
     1 Subject: Announcing Isabelle2009-2
     1 Subject: Announcing Isabelle2011
     2 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     3 
     4 Isabelle2009-2 is now available.
     4 Isabelle2011 is now available.
     5 
     5 
     6 This release improves upon Isabelle2009-1 in many respects, see the
     6 This version significantly improves upon Isabelle2009-2, see the NEWS
     7 NEWS file in the distribution for more details.  Some notable changes
     7 file in the distribution for more details.  Some notable changes are:
     8 are:
       
     9 
     8 
    10 * Explicit proof terms for type class reasoning.
     9 * Experimental Prover IDE based on Isabelle/Scala and jEdit.
    11 
    10 
    12 * Robust treatment of concrete syntax for different logical entities;
    11 * Coercive subtyping (configured in HOL/Complex_Main).
    13 mixfix syntax in local proof context.
       
    14 
    12 
    15 * Type declarations and notation within local theory context.
    13 * HOL code generation: Scala as another target language.
    16 
    14 
    17 * HOL: package for quotient types.
    15 * HOL: partial_function definitions.
    18 
    16 
    19 * HOL code generation: simple concept for abstract datatypes obeying
    17 * HOL: various tool enhancements, including Quickcheck, Nitpick,
    20 invariants (e.g. red-black trees).
    18   Sledgehammer, SMT integration.
    21 
    19 
    22 * HOL: new development of the Reals using Cauchy Sequences.
    20 * HOL: various additions to theory library, including HOL-Algebra,
       
    21   Imperative_HOL Multivariate_Analysis, Probability.
    23 
    22 
    24 * HOL: reorganization of abstract algebra type class hierarchy.
    23 * HOLCF: reorganization of library and related tools.
    25 
    24 
    26 * HOL: substantial reorganization of main library and related tools.
    25 * HOL/SPARK: interactive proof environment for verification conditions
       
    26   generated by the SPARK Ada program verifier.
    27 
    27 
    28 * HOLCF: reorganization of 'domain' package.
    28 * Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
    29 
    29 
    30 
    30 
    31 You may get Isabelle2009-2 from the following mirror sites:
    31 You may get Isabelle2011 from the following mirror sites:
    32 
    32 
    33   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    33   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    34   Munich (Germany)     http://isabelle.in.tum.de/
    34   Munich (Germany)     http://isabelle.in.tum.de/
    35   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    35   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/