updated for Isabelle2005;
authorwenzelm
Wed Sep 21 11:19:16 2005 +0200 (2005-09-21)
changeset 17544929d157d4369
parent 17543 79cc33f5ed37
child 17545 1ba448f96af1
updated for Isabelle2005;
ANNOUNCE
     1.1 --- a/ANNOUNCE	Wed Sep 21 10:40:28 2005 +0200
     1.2 +++ b/ANNOUNCE	Wed Sep 21 11:19:16 2005 +0200
     1.3 @@ -1,53 +1,31 @@
     1.4 -Subject: Announcing Isabelle2004
     1.5 +Subject: Announcing Isabelle2005
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2004 is now available.
     1.9 +Isabelle2005 is now available.
    1.10 +
    1.11 +This release provides substantial advances over Isabelle2004.  Some
    1.12 +highlights are as follows (see the NEWS of the distribution for more
    1.13 +details):
    1.14 +
    1.15 +* Interpretation of locale expressions in theories, locales, and proof
    1.16 +contexts.
    1.17 +
    1.18 +* Substantial library improvements (HOL, HOL-Complex, HOLCF).
    1.19  
    1.20 -This release provides many improvements and a few substantial advances over
    1.21 -Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
    1.22 -(see the NEWS of the distribution for more details):
    1.23 +* Proof tools for transitivity reasoning.
    1.24 +
    1.25 +* General 'find_theorems' command (by term patterns, as
    1.26 +intro/elim/simp rules etc.).
    1.27 +
    1.28 +* Commands for generating adhoc draft documents.
    1.29 +
    1.30 +* Support for Unicode proof documents (UTF-8).
    1.31 +
    1.32 +* Major internal reorganizations and performance improvements.
    1.33  
    1.34  
    1.35 -* New image HOL4 with imported library from HOL4 system on top of
    1.36 -  HOL-Complex (about 2500 additional theorems). 
    1.37 -
    1.38 -* New theory Ring_and_Field with over 250 basic numerical laws, 
    1.39 -  all proved in axiomatic type classes for semirings, rings and fields.
    1.40 -
    1.41 -* Type "rat" of the rational numbers available in HOL-Complex.
    1.42 -
    1.43 -* New locale "ring" for non-commutative rings in HOL-Algebra.
    1.44 -
    1.45 -* New theory of matrices with an application to linear programming in
    1.46 -  HOL-Matrix.
    1.47 -
    1.48 -* Improved locales (named proof contexts), instantiation of locales.
    1.49 -
    1.50 -* Improved handling of linear and partial orders in simplifier.
    1.51 - 
    1.52 -* New "specification" command for definition by specification.
    1.53 -
    1.54 -* New Isar command "finalconsts" prevents constants being given a definition
    1.55 -  later.
    1.56 -
    1.57 -* Command "arith" now generates counterexamples for reals as well.
    1.58 -
    1.59 -* New "quickcheck" command to search for counterexamples of executable goals.
    1.60 -  (see HOL/ex/Quickcheck_Examples.thy)
    1.61 -
    1.62 -* New "refute" command to search for finite countermodels of goals.
    1.63 -  (see HOL/ex/Refute_Examples.thy)
    1.64 -
    1.65 -* Presentation and x-symbol enhancements, greek letters and sub/superscripts
    1.66 -  allowed in identifiers.
    1.67 -
    1.68 -
    1.69 -You may get Isabelle2004 from the following mirror sites:
    1.70 +You may get Isabelle2005 from the following mirror sites:
    1.71  
    1.72    Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    1.73    Munich (Germany)     http://isabelle.in.tum.de/dist/
    1.74    Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    1.75 -
    1.76 -Gerwin Klein
    1.77 -Tobias Nipkow
    1.78 -Larry Paulson