ANNOUNCE
author wenzelm
Mon Mar 21 21:05:08 2011 +0100 (2011-03-21)
changeset 42044 17dc2c6edb93
parent 41605 7d035da21e9c
child 44801 a0459c50cfc9
permissions -rw-r--r--
tuned;
     1 Subject: Announcing Isabelle2011
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2011 is now available.
     5 
     6 This version significantly improves upon Isabelle2009-2, see the NEWS
     7 file in the distribution for more details.  Some notable changes are:
     8 
     9 * Experimental Prover IDE based on Isabelle/Scala and jEdit.
    10 
    11 * Coercive subtyping (configured in HOL/Complex_Main).
    12 
    13 * HOL code generation: Scala as another target language.
    14 
    15 * HOL: partial_function definitions.
    16 
    17 * HOL: various tool enhancements, including Quickcheck, Nitpick,
    18   Sledgehammer, SMT integration.
    19 
    20 * HOL: various additions to theory library, including HOL-Algebra,
    21   Imperative_HOL, Multivariate_Analysis, Probability.
    22 
    23 * HOLCF: reorganization of library and related tools.
    24 
    25 * HOL/SPARK: interactive proof environment for verification conditions
    26   generated by the SPARK Ada program verifier.
    27 
    28 * Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
    29 
    30 
    31 You may get Isabelle2011 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/