ANNOUNCE
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 14023 180f01d9df2c
child 14614 196ff8d245bf
permissions -rw-r--r--
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
     1
Subject: Announcing Isabelle2003
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     2
To: isabelle-users@cl.cam.ac.uk
b7698bd95a94 template;
wenzelm
parents:
diff changeset
     3
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
     4
Isabelle2003 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
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
     7
Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
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
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    10
 * New framework for extracting programs from constructive proofs in HOL.
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    11
   (Berghofer)
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    12
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    13
 * Improved simplifier. The premises of a goal are completely
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    14
   interreduced, ie simplified wrt each other. (Berghofer)
10161
4a3cd038aff8 draft for 99-1;
wenzelm
parents: 9928
diff changeset
    15
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    16
 * Presburger arithmetic. Method arith can deal with quantified formulae over
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    17
   nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    18
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    19
 * New command to find all rules whose conclusion matches the current goal.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    20
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    21
 * New command to trace why unification failed.
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    22
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    23
 * Locales (named proof contexts).  The new implementation is fully
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    24
   integrated with Isar's notion of proof context, and locale specifications
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    25
   produce predicate definitions that allow to work with locales in more
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    26
   flexible ways. (Wenzel)
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    27
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    28
 * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    29
   algebraic developments in HOL.  Currently covers group and ring theory.
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    30
   (Ballarin, Kammüller, Paulson)
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    31
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    32
 * HOL/Complex defines the type "complex" of the complex numbers, with numeric
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    33
   constants and some complex analysis, including nonstandard analysis.  The
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    34
   image HOL-Complex should be used for developments involving the real
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    35
   numbers too.  Gauge integration and hyperreal logarithms have recently
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    36
   been added. (Fleuriot)
10162
wenzelm
parents: 10161
diff changeset
    37
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    38
 * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    39
   Gray and Kramer)
12983
7d13480ee668 more stuff;
wenzelm
parents: 12964
diff changeset
    40
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    41
 * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
14022
3407f1b807ce tweaked
paulson
parents: 14021
diff changeset
    42
   of choice is mechanized using Isabelle/ZF, following Kunen's well-known
14021
24bf519625ab *** empty log message ***
nipkow
parents: 13045
diff changeset
    43
   textbook "Set Theory". (Paulson)
10166
wenzelm
parents: 10165
diff changeset
    44
14022
3407f1b807ce tweaked
paulson
parents: 14021
diff changeset
    45
You may get Isabelle2003 from the following mirror sites:
9928
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    46
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    47
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
b7698bd95a94 template;
wenzelm
parents:
diff changeset
    48
  Munich (Germany)  http://isabelle.in.tum.de/dist/
14023
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    49
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    50
Gerwin Klein
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    51
Tobias Nipkow
180f01d9df2c *** empty log message ***
nipkow
parents: 14022
diff changeset
    52
Larry Paulson