ANNOUNCE

converted to Isar theory format;

+
−Subject: Announcing Isabelle2004
+
−To: [e-mail]
+
−
+
−Isabelle2004 is now available.
+
−
+
−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):
+
−
+
−
+
−* 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:
+
−
+
−  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