removed obsolete sanity check -- Sign.certify_sort is stable;
Subject: Announcing Isabelle2009-1To: isabelle-users@cl.cam.ac.ukIsabelle2009-1 is now available.This release improves upon Isabelle2009 in many ways, see the NEWSfile in the distribution for more details. Some important changesare:* 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 logicwith 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 Kodkodrelational 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 realarithmetic, 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 compilererrors and run-time exceptions, including detailed source positions.* Parallel checking of nested Isar proofs, with improved scalabilityup 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/