ANNOUNCE
author paulson
Mon May 12 18:50:07 2003 +0200 (2003-05-12)
changeset 14022 3407f1b807ce
parent 14021 24bf519625ab
child 14023 180f01d9df2c
permissions -rw-r--r--
tweaked
nipkow@14021
     1
Subject: Announcing Isabelle2003
wenzelm@9928
     2
To: isabelle-users@cl.cam.ac.uk
wenzelm@9928
     3
nipkow@14021
     4
Isabelle2003 is now available.
wenzelm@12927
     5
nipkow@14021
     6
This release provides many improvements and a few substantial advances over
nipkow@14021
     7
Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
nipkow@14021
     8
(see the NEWS of the distribution for more details):
wenzelm@12927
     9
nipkow@14021
    10
 * New framework for extracting programs from constructive proofs in HOL.
nipkow@14021
    11
   (Berghofer)
wenzelm@12983
    12
nipkow@14021
    13
 * Improved simplifier. The premises of a goal are completely
nipkow@14021
    14
   interreduced, ie simplified wrt each other. (Berghofer)
wenzelm@10161
    15
nipkow@14021
    16
 * Presburger arithmetic. Method arith can deal with quantified formulae over
nipkow@14021
    17
   nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
wenzelm@12983
    18
nipkow@14021
    19
 * New command to find all rules whose conclusion matches the current goal.
wenzelm@12983
    20
nipkow@14021
    21
 * New command to trace why unification failed.
wenzelm@12983
    22
nipkow@14021
    23
 * Locales (named proof contexts).  The new implementation is fully
nipkow@14021
    24
   integrated with Isar's notion of proof context, and locale specifications
nipkow@14021
    25
   produce predicate definitions that allow to work with locales in more
nipkow@14021
    26
   flexible ways. (Wenzel)
wenzelm@12983
    27
nipkow@14021
    28
 * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
nipkow@14021
    29
   algebraic developments in HOL.  Currently covers group and ring theory.
nipkow@14021
    30
   (Ballarin, Kammüller, Paulson)
wenzelm@9928
    31
nipkow@14021
    32
 * HOL/Complex defines the type "complex" of the complex numbers, with numeric
nipkow@14021
    33
   constants and some complex analysis, including nonstandard analysis.  The
nipkow@14021
    34
   image HOL-Complex should be used for developments involving the real
nipkow@14021
    35
   numbers too.  Gauge integration and hyperreal logarithms have recently
nipkow@14021
    36
   been added. (Fleuriot)
wenzelm@10162
    37
nipkow@14021
    38
 * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
nipkow@14021
    39
   Gray and Kramer)
wenzelm@12983
    40
nipkow@14021
    41
 * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
paulson@14022
    42
   of choice is mechanized using Isabelle/ZF, following Kunen's well-known
nipkow@14021
    43
   textbook "Set Theory". (Paulson)
wenzelm@10166
    44
paulson@14022
    45
You may get Isabelle2003 from the following mirror sites:
wenzelm@9928
    46
wenzelm@9928
    47
  Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928
    48
  Munich (Germany)  http://isabelle.in.tum.de/dist/