ANNOUNCE
changeset 33866 34e45b2afe43
parent 33842 efa1b89c79e0
child 33873 e9120a7b2779
     1.1 --- a/ANNOUNCE	Sun Nov 22 14:13:18 2009 +0100
     1.2 +++ b/ANNOUNCE	Mon Nov 23 19:03:16 2009 +0100
     1.3 @@ -7,8 +7,24 @@
     1.4  file in the distribution for more details.  Some important changes
     1.5  are:
     1.6  
     1.7 -* FIXME
     1.8 +* Proof method "smt" for a combination of first-order logic with equality,
     1.9 +linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
    1.10  
    1.11 +* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
    1.12 +
    1.13 +* Predicate compiler turning inductive into (executable) equational specifications.
    1.14 +
    1.15 +* Refined number theory.
    1.16 +
    1.17 +* Various parts of multivariate analysis.
    1.18 +
    1.19 +* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.20 +
    1.21 +* Revised tutorial on locales.
    1.22 +
    1.23 +* New definitional domain package for HOLCF.
    1.24 +
    1.25 +* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
    1.26  
    1.27  You may get Isabelle2009-1 from the following mirror sites:
    1.28