author | wenzelm |
Tue, 27 Apr 2010 14:41:27 +0200 | |
changeset 36418 | 752ee03427c2 |
parent 33914 | d17f447fec02 |
child 37159 | 07f3f5a03e98 |
permissions | -rw-r--r-- |
Subject: Announcing Isabelle2009-1 To: isabelle-users@cl.cam.ac.uk Isabelle2009-1 is now available. This release improves upon Isabelle2009 in many ways, see the NEWS file in the distribution for more details. Some important changes are: * Isabelle tool "wwwfind" provides web interface for 'find_theorems' on a given logic image. * HOL-SMT: proof method "smt" for a combination of first-order logic with equality, linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors. * HOL-Boogie: an interactive prover back-end for Boogie and VCC. * HOL: counterexample generator tool Nitpick based on the Kodkod relational model finder. * HOL: predicate compiler turning inductive into (executable) equational specifications. * HOL: refined number theory. * HOL: various parts of multivariate analysis. * HOL-Library: proof method "sos" (sum of squares) for nonlinear real arithmetic, based on external semidefinite programming solvers. * HOLCF: new definitional domain package. * Revised tutorial on locales. * ML: tacticals for subgoal focus. * ML: support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions. * Parallel checking of nested Isar proofs, with improved scalability up to 8 cores. You may get Isabelle2009-1 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/