added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
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/