Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.
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