ANNOUNCE
changeset 37159 07f3f5a03e98
parent 33914 d17f447fec02
child 37317 5164c4ec787b
     1.1 --- a/ANNOUNCE	Thu May 27 21:37:42 2010 +0200
     1.2 +++ b/ANNOUNCE	Fri May 28 11:23:34 2010 +0200
     1.3 @@ -1,48 +1,16 @@
     1.4 -Subject: Announcing Isabelle2009-1
     1.5 +Subject: Announcing Isabelle2009-2
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2009-1 is now available.
     1.9 +Isabelle2009-2 is now available.
    1.10  
    1.11 -This release improves upon Isabelle2009 in many ways, see the NEWS
    1.12 -file in the distribution for more details.  Some important changes
    1.13 +This release improves upon Isabelle2009-1 in many respects, see the
    1.14 +NEWS file in the distribution for more details.  Some notable changes
    1.15  are:
    1.16  
    1.17 -* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
    1.18 -on a given logic image.
    1.19 -
    1.20 -* HOL-SMT: proof method "smt" for a combination of first-order logic
    1.21 -with equality, linear and nonlinear (natural/integer/real) arithmetic,
    1.22 -and fixed-size bitvectors.
    1.23 -
    1.24 -* HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.25 -
    1.26 -* HOL: counterexample generator tool Nitpick based on the Kodkod
    1.27 -relational model finder.
    1.28 -
    1.29 -* HOL: predicate compiler turning inductive into (executable)
    1.30 -equational specifications.
    1.31 -
    1.32 -* HOL: refined number theory.
    1.33 -
    1.34 -* HOL: various parts of multivariate analysis.
    1.35 -
    1.36 -* HOL-Library: proof method "sos" (sum of squares) for nonlinear real
    1.37 -arithmetic, based on external semidefinite programming solvers.
    1.38 -
    1.39 -* HOLCF: new definitional domain package.
    1.40 -
    1.41 -* Revised tutorial on locales.
    1.42 -
    1.43 -* ML: tacticals for subgoal focus.
    1.44 -
    1.45 -* ML: support for Poly/ML 5.3.0, with improved reporting of compiler
    1.46 -errors and run-time exceptions, including detailed source positions.
    1.47 -
    1.48 -* Parallel checking of nested Isar proofs, with improved scalability
    1.49 -up to 8 cores.
    1.50 +* FIXME
    1.51  
    1.52  
    1.53 -You may get Isabelle2009-1 from the following mirror sites:
    1.54 +You may get Isabelle2009-2 from the following mirror sites:
    1.55  
    1.56    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.57    Munich (Germany)     http://isabelle.in.tum.de/