updated for Isabelle2005;
Wed, 21 Sep 2005 11:19:16 +0200
changeset 17544 929d157d4369
parent 17543 79cc33f5ed37
child 17545 1ba448f96af1
updated for Isabelle2005;
--- a/ANNOUNCE	Wed Sep 21 10:40:28 2005 +0200
+++ b/ANNOUNCE	Wed Sep 21 11:19:16 2005 +0200
@@ -1,53 +1,31 @@
-Subject: Announcing Isabelle2004
+Subject: Announcing Isabelle2005
 To: isabelle-users@cl.cam.ac.uk
-Isabelle2004 is now available.
+Isabelle2005 is now available.
+This release provides substantial advances over Isabelle2004.  Some
+highlights are as follows (see the NEWS of the distribution for more
+* Interpretation of locale expressions in theories, locales, and proof
+* Substantial library improvements (HOL, HOL-Complex, HOLCF).
-This release provides many improvements and a few substantial advances over
-Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
-(see the NEWS of the distribution for more details):
+* Proof tools for transitivity reasoning.
+* General 'find_theorems' command (by term patterns, as
+intro/elim/simp rules etc.).
+* Commands for generating adhoc draft documents.
+* Support for Unicode proof documents (UTF-8).
+* Major internal reorganizations and performance improvements.
-* New image HOL4 with imported library from HOL4 system on top of
-  HOL-Complex (about 2500 additional theorems). 
-* New theory Ring_and_Field with over 250 basic numerical laws, 
-  all proved in axiomatic type classes for semirings, rings and fields.
-* Type "rat" of the rational numbers available in HOL-Complex.
-* New locale "ring" for non-commutative rings in HOL-Algebra.
-* New theory of matrices with an application to linear programming in
-  HOL-Matrix.
-* Improved locales (named proof contexts), instantiation of locales.
-* Improved handling of linear and partial orders in simplifier.
-* New "specification" command for definition by specification.
-* New Isar command "finalconsts" prevents constants being given a definition
-  later.
-* Command "arith" now generates counterexamples for reals as well.
-* New "quickcheck" command to search for counterexamples of executable goals.
-  (see HOL/ex/Quickcheck_Examples.thy)
-* New "refute" command to search for finite countermodels of goals.
-  (see HOL/ex/Refute_Examples.thy)
-* Presentation and x-symbol enhancements, greek letters and sub/superscripts
-  allowed in identifiers.
-You may get Isabelle2004 from the following mirror sites:
+You may get Isabelle2005 from the following mirror sites:
   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
   Munich (Germany)     http://isabelle.in.tum.de/dist/
   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
-Gerwin Klein
-Tobias Nipkow
-Larry Paulson