ANNOUNCE
author bulwahn
Mon Nov 23 21:56:07 2009 +0100 (2009-11-23)
changeset 33871 caab5399bb2d
parent 33866 34e45b2afe43
child 33873 e9120a7b2779
permissions -rw-r--r--
merged
     1 Subject: Announcing Isabelle2009-1
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2009-1 is now available.
     5 
     6 This release improves upon Isabelle2009 in many ways, see the NEWS
     7 file in the distribution for more details.  Some important changes
     8 are:
     9 
    10 * Proof method "smt" for a combination of first-order logic with equality,
    11 linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
    12 
    13 * Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
    14 
    15 * Predicate compiler turning inductive into (executable) equational specifications.
    16 
    17 * Refined number theory.
    18 
    19 * Various parts of multivariate analysis.
    20 
    21 * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    22 
    23 * Revised tutorial on locales.
    24 
    25 * New definitional domain package for HOLCF.
    26 
    27 * Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
    28 
    29 You may get Isabelle2009-1 from the following mirror sites:
    30 
    31   Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    32   Munich (Germany)     http://isabelle.in.tum.de/
    33   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/