ANNOUNCE
author wenzelm
Mon Jan 17 22:54:08 2011 +0100 (2011-01-17)
changeset 41604 313b0033034a
parent 37353 b6222a65bacf
child 41605 7d035da21e9c
permissions -rw-r--r--
some announcement;
     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/