ANNOUNCE
author nipkow
Sat Apr 17 14:51:00 2004 +0200 (2004-04-17)
changeset 14614 196ff8d245bf
parent 14023 180f01d9df2c
child 14616 b167b1b848d8
permissions -rw-r--r--
2003 -> 2004
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@12983
    10
nipkow@14614
    11
* New theory Ring_and_Field with over 250 basic numerical laws, 
nipkow@14614
    12
  all proved in axiomatic type classes for semirings, rings and fields.
nipkow@14614
    13
nipkow@14614
    14
* Type "rat" of the rational numbers available in HOL-Complex.
wenzelm@10161
    15
nipkow@14614
    16
* New locale "ring" for non-commutative rings in HOL-Algebra.
wenzelm@12983
    17
nipkow@14614
    18
* New theory of matrices with an application to linear programming in
nipkow@14614
    19
  HOL-Matrix.
wenzelm@12983
    20
nipkow@14614
    21
* Improved locales (named proof contexts), instantiation of locales.
wenzelm@12983
    22
nipkow@14614
    23
* Improved handling of linear and partial orders in simplifier.
nipkow@14614
    24
 
nipkow@14614
    25
* New "specification" command for definition by specification.
wenzelm@12983
    26
nipkow@14614
    27
* New Isar command "finalconsts" prevents constants being given a definition
nipkow@14614
    28
  later.
nipkow@14614
    29
nipkow@14614
    30
* Command "arith" now generates counterexamples for reals as well.
wenzelm@9928
    31
nipkow@14614
    32
* New "quickcheck" command to search for counterexamples of executable goals.
nipkow@14614
    33
  (see HOL/ex/Quickcheck_Examples.thy)
wenzelm@10162
    34
nipkow@14614
    35
* New "refute" command to search for finite countermodels of goals.
nipkow@14614
    36
  (see HOL/ex/Refute_Examples.thy)
wenzelm@12983
    37
nipkow@14614
    38
* Presentation and x-symbol enhancements, greek letters and sub/superscripts
nipkow@14614
    39
  allowed in identifiers.
nipkow@14614
    40
wenzelm@10166
    41
paulson@14022
    42
You may get Isabelle2003 from the following mirror sites:
wenzelm@9928
    43
wenzelm@9928
    44
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928
    45
  Munich (Germany)  http://isabelle.in.tum.de/dist/
nipkow@14023
    46
nipkow@14023
    47
Gerwin Klein
nipkow@14023
    48
Tobias Nipkow
nipkow@14023
    49
Larry Paulson