made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
Subject: Announcing Isabelle2011
To: isabelle-users@cl.cam.ac.uk
Isabelle2011 is now available.
This version significantly improves upon Isabelle2009-2, see the NEWS
file in the distribution for more details. Some notable changes are:
* Experimental Prover IDE based on Isabelle/Scala and jEdit.
* Coercive subtyping (configured in HOL/Complex_Main).
* HOL code generation: Scala as another target language.
* HOL: partial_function definitions.
* HOL: various tool enhancements, including Quickcheck, Nitpick,
Sledgehammer, SMT integration.
* HOL: various additions to theory library, including HOL-Algebra,
Imperative_HOL, Multivariate_Analysis, Probability.
* HOLCF: reorganization of library and related tools.
* HOL/SPARK: interactive proof environment for verification conditions
generated by the SPARK Ada program verifier.
* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
You may get Isabelle2011 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/