ANNOUNCE

remove more duplicate lemmas

+
−Subject: Announcing Isabelle2011
+
−To: [e-mail]
+
−
+
−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/