ANNOUNCE
author kleing
Sat Apr 17 14:57:50 2004 +0200 (2004-04-17)
changeset 14616 b167b1b848d8
parent 14614 196ff8d245bf
child 14624 9b3397a848c3
permissions -rw-r--r--
added sydney mirror
     1 Subject: Announcing Isabelle2004
     2 To: isabelle-users@cl.cam.ac.uk
     3 
     4 Isabelle2004 is now available.
     5 
     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):
     9 
    10 
    11 * New theory Ring_and_Field with over 250 basic numerical laws, 
    12   all proved in axiomatic type classes for semirings, rings and fields.
    13 
    14 * Type "rat" of the rational numbers available in HOL-Complex.
    15 
    16 * New locale "ring" for non-commutative rings in HOL-Algebra.
    17 
    18 * New theory of matrices with an application to linear programming in
    19   HOL-Matrix.
    20 
    21 * Improved locales (named proof contexts), instantiation of locales.
    22 
    23 * Improved handling of linear and partial orders in simplifier.
    24  
    25 * New "specification" command for definition by specification.
    26 
    27 * New Isar command "finalconsts" prevents constants being given a definition
    28   later.
    29 
    30 * Command "arith" now generates counterexamples for reals as well.
    31 
    32 * New "quickcheck" command to search for counterexamples of executable goals.
    33   (see HOL/ex/Quickcheck_Examples.thy)
    34 
    35 * New "refute" command to search for finite countermodels of goals.
    36   (see HOL/ex/Refute_Examples.thy)
    37 
    38 * Presentation and x-symbol enhancements, greek letters and sub/superscripts
    39   allowed in identifiers.
    40 
    41 
    42 You may get Isabelle2004 from the following mirror sites:
    43 
    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/
    47 
    48 Gerwin Klein
    49 Tobias Nipkow
    50 Larry Paulson