1 Subject: Announcing Isabelle2004
2 To: isabelle-users@cl.cam.ac.uk
4 Isabelle2004 is now available.
6 This release provides many improvements and a few substantial advances over
7 Isabelle2003. The most prominent highlights of Isabelle2004 are as follows
8 (see the NEWS of the distribution for more details):
11 * New theory Ring_and_Field with over 250 basic numerical laws,
12 all proved in axiomatic type classes for semirings, rings and fields.
14 * Type "rat" of the rational numbers available in HOL-Complex.
16 * New locale "ring" for non-commutative rings in HOL-Algebra.
18 * New theory of matrices with an application to linear programming in
21 * Improved locales (named proof contexts), instantiation of locales.
23 * Improved handling of linear and partial orders in simplifier.
25 * New "specification" command for definition by specification.
27 * New Isar command "finalconsts" prevents constants being given a definition
30 * Command "arith" now generates counterexamples for reals as well.
32 * New "quickcheck" command to search for counterexamples of executable goals.
33 (see HOL/ex/Quickcheck_Examples.thy)
35 * New "refute" command to search for finite countermodels of goals.
36 (see HOL/ex/Refute_Examples.thy)
38 * Presentation and x-symbol enhancements, greek letters and sub/superscripts
39 allowed in identifiers.
42 You may get Isabelle2004 from the following mirror sites:
44 Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
45 Munich (Germany) http://isabelle.in.tum.de/dist/
46 Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/