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