1) Fixed bug in Defs.merge_edges_1.
2) Major optimization of Defs.define: do not store dependencies between constants that
cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to
theories that define their constants in HOL-light / HOL4 style.
3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.
Subject: Announcing Isabelle2004
To: isabelle-users@cl.cam.ac.uk
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