ANNOUNCE
author obua
Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440 df77edc4f5d0
parent 14624 9b3397a848c3
child 17544 929d157d4369
permissions -rw-r--r--
fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
     1
Subject: Announcing Isabelle2004
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
     4
Isabelle2004 is now available.
12927
wenzelm
parents: 11600
diff changeset
     5
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
     6
This release provides many improvements and a few substantial advances over
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
     7
Isabelle2003.  The most prominent highlights of Isabelle2004 are as follows
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
     8
(see the NEWS of the distribution for more details):
12927
wenzelm
parents: 11600
diff changeset
     9
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    10
14624
9b3397a848c3 add HOL4
kleing
parents: 14616
diff changeset
    11
* New image HOL4 with imported library from HOL4 system on top of
9b3397a848c3 add HOL4
kleing
parents: 14616
diff changeset
    12
  HOL-Complex (about 2500 additional theorems). 
9b3397a848c3 add HOL4
kleing
parents: 14616
diff changeset
    13
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    14
* New theory Ring_and_Field with over 250 basic numerical laws, 
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    15
  all proved in axiomatic type classes for semirings, rings and fields.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    16
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    17
* Type "rat" of the rational numbers available in HOL-Complex.
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    18
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    19
* New locale "ring" for non-commutative rings in HOL-Algebra.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    20
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    21
* New theory of matrices with an application to linear programming in
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    22
  HOL-Matrix.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    23
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    24
* Improved locales (named proof contexts), instantiation of locales.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    25
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    26
* Improved handling of linear and partial orders in simplifier.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    27
 
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    28
* New "specification" command for definition by specification.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    29
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    30
* New Isar command "finalconsts" prevents constants being given a definition
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    31
  later.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    32
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    33
* Command "arith" now generates counterexamples for reals as well.
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    34
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    35
* New "quickcheck" command to search for counterexamples of executable goals.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    36
  (see HOL/ex/Quickcheck_Examples.thy)
10162
wenzelm
parents: 10161
diff changeset
    37
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    38
* New "refute" command to search for finite countermodels of goals.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    39
  (see HOL/ex/Refute_Examples.thy)
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    40
14614
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    41
* Presentation and x-symbol enhancements, greek letters and sub/superscripts
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    42
  allowed in identifiers.
196ff8d245bf 2003 -> 2004
nipkow
parents: 14023
diff changeset
    43
10166
wenzelm
parents: 10165
diff changeset
    44
14616
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    45
You may get Isabelle2004 from the following mirror sites:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    46
14616
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    47
  Cambridge (UK)       http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    48
  Munich (Germany)     http://isabelle.in.tum.de/dist/
b167b1b848d8 added sydney mirror
kleing
parents: 14614
diff changeset
    49
  Sydney (Australia)   http://mirror.cse.unsw.edu.au/pub/isabelle/
14023
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    50
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    51
Gerwin Klein
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    52
Tobias Nipkow
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    53
Larry Paulson