author | paulson |
Thu, 02 Sep 2004 16:52:21 +0200 | |
changeset 15172 | 73069e033a0b |
parent 14624 | 9b3397a848c3 |
child 17544 | 929d157d4369 |
permissions | -rw-r--r-- |
nipkow@14614 | 1 |
Subject: Announcing Isabelle2004 |
wenzelm@9928 | 2 |
To: isabelle-users@cl.cam.ac.uk |
wenzelm@9928 | 3 |
|
nipkow@14614 | 4 |
Isabelle2004 is now available. |
wenzelm@12927 | 5 |
|
nipkow@14021 | 6 |
This release provides many improvements and a few substantial advances over |
nipkow@14614 | 7 |
Isabelle2003. The most prominent highlights of Isabelle2004 are as follows |
nipkow@14021 | 8 |
(see the NEWS of the distribution for more details): |
wenzelm@12927 | 9 |
|
wenzelm@9928 | 10 |
|
kleing@14624 | 11 |
* New image HOL4 with imported library from HOL4 system on top of |
kleing@14624 | 12 |
HOL-Complex (about 2500 additional theorems). |
kleing@14624 | 13 |
|
nipkow@14614 | 14 |
* New theory Ring_and_Field with over 250 basic numerical laws, |
nipkow@14614 | 15 |
all proved in axiomatic type classes for semirings, rings and fields. |
wenzelm@9928 | 16 |
|
nipkow@14614 | 17 |
* Type "rat" of the rational numbers available in HOL-Complex. |
wenzelm@10161 | 18 |
|
nipkow@14614 | 19 |
* New locale "ring" for non-commutative rings in HOL-Algebra. |
wenzelm@10161 | 20 |
|
nipkow@14614 | 21 |
* New theory of matrices with an application to linear programming in |
nipkow@14614 | 22 |
HOL-Matrix. |
wenzelm@12964 | 23 |
|
nipkow@14614 | 24 |
* Improved locales (named proof contexts), instantiation of locales. |
wenzelm@12983 | 25 |
|
nipkow@14614 | 26 |
* Improved handling of linear and partial orders in simplifier. |
nipkow@14614 | 27 |
|
nipkow@14614 | 28 |
* New "specification" command for definition by specification. |
wenzelm@12983 | 29 |
|
nipkow@14614 | 30 |
* New Isar command "finalconsts" prevents constants being given a definition |
nipkow@14614 | 31 |
later. |
wenzelm@12983 | 32 |
|
nipkow@14614 | 33 |
* Command "arith" now generates counterexamples for reals as well. |
wenzelm@12983 | 34 |
|
nipkow@14614 | 35 |
* New "quickcheck" command to search for counterexamples of executable goals. |
nipkow@14614 | 36 |
(see HOL/ex/Quickcheck_Examples.thy) |
nipkow@14614 | 37 |
|
nipkow@14614 | 38 |
* New "refute" command to search for finite countermodels of goals. |
nipkow@14614 | 39 |
(see HOL/ex/Refute_Examples.thy) |
nipkow@14614 | 40 |
|
nipkow@14614 | 41 |
* Presentation and x-symbol enhancements, greek letters and sub/superscripts |
nipkow@14614 | 42 |
allowed in identifiers. |
nipkow@14614 | 43 |
|
wenzelm@12983 | 44 |
|
kleing@14616 | 45 |
You may get Isabelle2004 from the following mirror sites: |
wenzelm@9928 | 46 |
|
kleing@14616 | 47 |
Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ |
kleing@14616 | 48 |
Munich (Germany) http://isabelle.in.tum.de/dist/ |
kleing@14616 | 49 |
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/ |
nipkow@14023 | 50 |
|
nipkow@14023 | 51 |
Gerwin Klein |
nipkow@14023 | 52 |
Tobias Nipkow |
nipkow@14023 | 53 |
Larry Paulson |