isabelle: ANNOUNCE@7d69154d824b (annotated)

41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	1	Subject: Announcing Isabelle2011
9928 b7698bd95a94 template; wenzelm parents: diff changeset	2	To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template; wenzelm parents: diff changeset	3
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	4	Isabelle2011 is now available.
17544 929d157d4369 updated for Isabelle2005; wenzelm parents: 14624 diff changeset	5
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	6	This version significantly improves upon Isabelle2009-2, see the NEWS
313b0033034a some announcement; wenzelm parents: 37353 diff changeset	7	file in the distribution for more details. Some notable changes are:
27007 c1960cad5017 added some notable improvements; wenzelm parents: 27005 diff changeset	8
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	9	* Experimental Prover IDE based on Isabelle/Scala and jEdit.
313b0033034a some announcement; wenzelm parents: 37353 diff changeset	10
313b0033034a some announcement; wenzelm parents: 37353 diff changeset	11	* Coercive subtyping (configured in HOL/Complex_Main).
37317 5164c4ec787b first proposal for a announcement haftmann parents: 37159 diff changeset	12
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	13	* HOL code generation: Scala as another target language.
37317 5164c4ec787b first proposal for a announcement haftmann parents: 37159 diff changeset	14
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	15	* HOL: partial_function definitions.
37353 b6222a65bacf tuned ANNOUNCEMENT; wenzelm parents: 37317 diff changeset	16
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	17	* HOL: various tool enhancements, including Quickcheck, Nitpick,
313b0033034a some announcement; wenzelm parents: 37353 diff changeset	18	Sledgehammer, SMT integration.
33873 e9120a7b2779 more tuning for release; wenzelm parents: 33866 diff changeset	19
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	20	* HOL: various additions to theory library, including HOL-Algebra,
41605 7d035da21e9c tuned; wenzelm parents: 41604 diff changeset	21	Imperative_HOL, Multivariate_Analysis, Probability.
37317 5164c4ec787b first proposal for a announcement haftmann parents: 37159 diff changeset	22
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	23	* HOLCF: reorganization of library and related tools.
37317 5164c4ec787b first proposal for a announcement haftmann parents: 37159 diff changeset	24
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	25	* HOL/SPARK: interactive proof environment for verification conditions
313b0033034a some announcement; wenzelm parents: 37353 diff changeset	26	generated by the SPARK Ada program verifier.
37353 b6222a65bacf tuned ANNOUNCEMENT; wenzelm parents: 37317 diff changeset	27
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	28	* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
37353 b6222a65bacf tuned ANNOUNCEMENT; wenzelm parents: 37317 diff changeset	29
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	30
41604 313b0033034a some announcement; wenzelm parents: 37353 diff changeset	31	You may get Isabelle2011 from the following mirror sites:
9928 b7698bd95a94 template; wenzelm parents: diff changeset	32
27085 dbf4f791953d adjusted location of cambridge website haftmann parents: 27066 diff changeset	33	Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
17696 eccdee8a0790 adjusted www links haftmann parents: 17692 diff changeset	34	Munich (Germany) http://isabelle.in.tum.de/
14616 b167b1b848d8 added sydney mirror kleing parents: 14614 diff changeset	35	Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/

author	paulson
	Mon, 30 May 2011 16:10:12 +0100
changeset 43077	7d69154d824b
parent 41605	7d035da21e9c
child 44801	a0459c50cfc9
permissions	-rw-r--r--