author huffman
Thu, 26 May 2005 02:23:27 +0200
changeset 16081 81a4b4a245b0
parent 14624 9b3397a848c3
child 17544 929d157d4369
permissions -rw-r--r--
cleaned up, added cpair_less and cpair_eq_pair, removed some obsolete stuff

Subject: Announcing Isabelle2004

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

* 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

* 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)
  Munich (Germany)
  Sydney (Australia)

Gerwin Klein
Tobias Nipkow
Larry Paulson