ANNOUNCE
changeset 17544 929d157d4369
parent 14624 9b3397a848c3
child 17572 81fcc0029761
equal deleted inserted replaced
17543:79cc33f5ed37 17544:929d157d4369
     1 Subject: Announcing Isabelle2004
     1 Subject: Announcing Isabelle2005
     2 To: isabelle-users@cl.cam.ac.uk
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     3 
     4 Isabelle2004 is now available.
     4 Isabelle2005 is now available.
     5 
     5 
     6 This release provides many improvements and a few substantial advances over
     6 This release provides substantial advances over Isabelle2004.  Some
     7 Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
     7 highlights are as follows (see the NEWS of the distribution for more
     8 (see the NEWS of the distribution for more details):
     8 details):
       
     9 
       
    10 * Interpretation of locale expressions in theories, locales, and proof
       
    11 contexts.
       
    12 
       
    13 * Substantial library improvements (HOL, HOL-Complex, HOLCF).
       
    14 
       
    15 * Proof tools for transitivity reasoning.
       
    16 
       
    17 * General 'find_theorems' command (by term patterns, as
       
    18 intro/elim/simp rules etc.).
       
    19 
       
    20 * Commands for generating adhoc draft documents.
       
    21 
       
    22 * Support for Unicode proof documents (UTF-8).
       
    23 
       
    24 * Major internal reorganizations and performance improvements.
     9 
    25 
    10 
    26 
    11 * New image HOL4 with imported library from HOL4 system on top of
    27 You may get Isabelle2005 from the following mirror sites:
    12   HOL-Complex (about 2500 additional theorems). 
       
    13 
       
    14 * New theory Ring_and_Field with over 250 basic numerical laws, 
       
    15   all proved in axiomatic type classes for semirings, rings and fields.
       
    16 
       
    17 * Type "rat" of the rational numbers available in HOL-Complex.
       
    18 
       
    19 * New locale "ring" for non-commutative rings in HOL-Algebra.
       
    20 
       
    21 * New theory of matrices with an application to linear programming in
       
    22   HOL-Matrix.
       
    23 
       
    24 * Improved locales (named proof contexts), instantiation of locales.
       
    25 
       
    26 * Improved handling of linear and partial orders in simplifier.
       
    27  
       
    28 * New "specification" command for definition by specification.
       
    29 
       
    30 * New Isar command "finalconsts" prevents constants being given a definition
       
    31   later.
       
    32 
       
    33 * Command "arith" now generates counterexamples for reals as well.
       
    34 
       
    35 * New "quickcheck" command to search for counterexamples of executable goals.
       
    36   (see HOL/ex/Quickcheck_Examples.thy)
       
    37 
       
    38 * New "refute" command to search for finite countermodels of goals.
       
    39   (see HOL/ex/Refute_Examples.thy)
       
    40 
       
    41 * Presentation and x-symbol enhancements, greek letters and sub/superscripts
       
    42   allowed in identifiers.
       
    43 
       
    44 
       
    45 You may get Isabelle2004 from the following mirror sites:
       
    46 
    28 
    47   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    29   Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
    48   Munich (Germany)     http://isabelle.in.tum.de/dist/
    30   Munich (Germany)     http://isabelle.in.tum.de/dist/
    49   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    31   Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
    50 
       
    51 Gerwin Klein
       
    52 Tobias Nipkow
       
    53 Larry Paulson