summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

ANNOUNCE

author | huffman |

Thu, 14 Jul 2005 01:04:30 +0200 | |

changeset 16823 | 13f3768a6f14 |

parent 14624 | 9b3397a848c3 |

child 17544 | 929d157d4369 |

permissions | -rw-r--r-- |

simplified proof of cont_Iwhen3

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