isabelle: ANNOUNCE@37e34f315057 (annotated)

14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	1	Subject: Announcing Isabelle2004
9928 b7698bd95a94 template; wenzelm parents: diff changeset	2	To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template; wenzelm parents: diff changeset	3
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	4	Isabelle2004 is now available.
12927 b7c916bf3332 tuned; wenzelm parents: 11600 diff changeset	5
14021 24bf519625ab * empty log message * nipkow parents: 13045 diff changeset	6	This release provides many improvements and a few substantial advances over
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	7	Isabelle2003. The most prominent highlights of Isabelle2004 are as follows
14021 24bf519625ab * empty log message * nipkow parents: 13045 diff changeset	8	(see the NEWS of the distribution for more details):
12927 b7c916bf3332 tuned; wenzelm parents: 11600 diff changeset	9
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	10
14624 9b3397a848c3 add HOL4 kleing parents: 14616 diff changeset	11	* New image HOL4 with imported library from HOL4 system on top of
9b3397a848c3 add HOL4 kleing parents: 14616 diff changeset	12	HOL-Complex (about 2500 additional theorems).
9b3397a848c3 add HOL4 kleing parents: 14616 diff changeset	13
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	14	* New theory Ring_and_Field with over 250 basic numerical laws,
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	15	all proved in axiomatic type classes for semirings, rings and fields.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	16
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	17	* Type "rat" of the rational numbers available in HOL-Complex.
10161 4a3cd038aff8 draft for 99-1; wenzelm parents: 9928 diff changeset	18
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	19	* New locale "ring" for non-commutative rings in HOL-Algebra.
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	20
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	21	* New theory of matrices with an application to linear programming in
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	22	HOL-Matrix.
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	23
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	24	* Improved locales (named proof contexts), instantiation of locales.
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	25
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	26	* Improved handling of linear and partial orders in simplifier.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	27
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	28	* New "specification" command for definition by specification.
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	29
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	30	* New Isar command "finalconsts" prevents constants being given a definition
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	31	later.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	32
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	33	* Command "arith" now generates counterexamples for reals as well.
9928 b7698bd95a94 template; wenzelm parents: diff changeset	34
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	35	* New "quickcheck" command to search for counterexamples of executable goals.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	36	(see HOL/ex/Quickcheck_Examples.thy)
10162 947b7b8b0a69 tuned; wenzelm parents: 10161 diff changeset	37
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	38	* New "refute" command to search for finite countermodels of goals.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	39	(see HOL/ex/Refute_Examples.thy)
12983 7d13480ee668 more stuff; wenzelm parents: 12964 diff changeset	40
14614 196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	41	* Presentation and x-symbol enhancements, greek letters and sub/superscripts
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	42	allowed in identifiers.
196ff8d245bf 2003 -> 2004 nipkow parents: 14023 diff changeset	43
10166 fb99cee36240 tuned; wenzelm parents: 10165 diff changeset	44
14616 b167b1b848d8 added sydney mirror kleing parents: 14614 diff changeset	45	You may get Isabelle2004 from the following mirror sites:
9928 b7698bd95a94 template; wenzelm parents: diff changeset	46
14616 b167b1b848d8 added sydney mirror kleing parents: 14614 diff changeset	47	Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
b167b1b848d8 added sydney mirror kleing parents: 14614 diff changeset	48	Munich (Germany) http://isabelle.in.tum.de/dist/
b167b1b848d8 added sydney mirror kleing parents: 14614 diff changeset	49	Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
14023 180f01d9df2c * empty log message * nipkow parents: 14022 diff changeset	50
180f01d9df2c * empty log message * nipkow parents: 14022 diff changeset	51	Gerwin Klein
180f01d9df2c * empty log message * nipkow parents: 14022 diff changeset	52	Tobias Nipkow
180f01d9df2c * empty log message * nipkow parents: 14022 diff changeset	53	Larry Paulson

author	obua
	Mon, 01 Aug 2005 11:39:33 +0200
changeset 16966	37e34f315057
parent 14624	9b3397a848c3
child 17544	929d157d4369
permissions	-rw-r--r--