ANNOUNCE
changeset 33873 e9120a7b2779
parent 33866 34e45b2afe43
child 33881 d8958955ecb5
     1.1 --- a/ANNOUNCE	Mon Nov 23 22:35:54 2009 +0100
     1.2 +++ b/ANNOUNCE	Mon Nov 23 22:47:08 2009 +0100
     1.3 @@ -7,24 +7,35 @@
     1.4  file in the distribution for more details.  Some important changes
     1.5  are:
     1.6  
     1.7 -* Proof method "smt" for a combination of first-order logic with equality,
     1.8 -linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
     1.9 -
    1.10 -* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
    1.11 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
    1.12 +on a given logic image.
    1.13  
    1.14 -* Predicate compiler turning inductive into (executable) equational specifications.
    1.15 -
    1.16 -* Refined number theory.
    1.17 -
    1.18 -* Various parts of multivariate analysis.
    1.19 +* HOL-SMT: proof method "smt" for a combination of first-order logic
    1.20 +with equality, linear and nonlinear (natural/integer/real) arithmetic,
    1.21 +and fixed-size bitvectors.
    1.22  
    1.23  * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.24  
    1.25 +* HOL: Counterexample generator tool Nitpick based on the Kodkod
    1.26 +relational model finder.
    1.27 +
    1.28 +* HOL: predicate compiler turning inductive into (executable)
    1.29 +equational specifications.
    1.30 +
    1.31 +* HOL: refined number theory.
    1.32 +
    1.33 +* HOL: various parts of multivariate analysis.
    1.34 +
    1.35 +* HOLCF: new definitional domain package.
    1.36 +
    1.37  * Revised tutorial on locales.
    1.38  
    1.39 -* New definitional domain package for HOLCF.
    1.40 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
    1.41 +errors and run-time exceptions, including detailed source positions.
    1.42  
    1.43 -* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
    1.44 +* Parallel checking of nested Isar proofs, with improved scalability
    1.45 +up to 8 cores.
    1.46 +
    1.47  
    1.48  You may get Isabelle2009-1 from the following mirror sites:
    1.49