ANNOUNCE
changeset 14021 24bf519625ab
parent 13045 1db0bdda1d32
child 14022 3407f1b807ce
     1.1 --- a/ANNOUNCE	Mon May 12 18:11:44 2003 +0200
     1.2 +++ b/ANNOUNCE	Mon May 12 18:42:21 2003 +0200
     1.3 @@ -1,73 +1,48 @@
     1.4 -
     1.5 -Subject: Announcing Isabelle2002
     1.6 +Subject: Announcing Isabelle2003
     1.7  To: isabelle-users@cl.cam.ac.uk
     1.8  
     1.9 -Isabelle2002 is now available.
    1.10 +Isabelle2003 is now available.
    1.11  
    1.12 -This release provides major improvements.  The Isar language has
    1.13 -reached a mature state; the core engine is able to record full proof
    1.14 -terms; many aspects of the library have been reworked; several
    1.15 -substantial case studies have been added.  Some changes may cause
    1.16 -incompatibility with earlier versions, but improve accessibility of
    1.17 -Isabelle for new users.
    1.18 +This release provides many improvements and a few substantial advances over
    1.19 +Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
    1.20 +(see the NEWS of the distribution for more details):
    1.21  
    1.22 -The most prominent highlights of Isabelle2002 are as follows (see the
    1.23 -NEWS of the distribution for more details).
    1.24 -
    1.25 -  * The Isabelle/HOL tutorial is to be published as LNCS 2283;
    1.26 -    Isabelle2002 is the official version to go along with that book
    1.27 -    (by Tobias Nipkow, Larry Paulson, Markus Wenzel).
    1.28 + * New framework for extracting programs from constructive proofs in HOL.
    1.29 +   (Berghofer)
    1.30  
    1.31 -  * Pure: explicit proof terms for all internal inferences;
    1.32 -    object-logics, proof tools etc. will benefit automatically
    1.33 -    (by Stefan Berghofer).
    1.34 + * Improved simplifier. The premises of a goal are completely
    1.35 +   interreduced, ie simplified wrt each other. (Berghofer)
    1.36  
    1.37 -  * Pure/Isar: proper integration of the locale package for modular
    1.38 -    theory development; additional support for rename/merge
    1.39 -    operations, and type-inference for structured specifications
    1.40 -    (by Markus Wenzel).
    1.41 + * Presburger arithmetic. Method arith can deal with quantified formulae over
    1.42 +   nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
    1.43  
    1.44 -  * Pure/Isar: streamlined cases/induction proof patterns
    1.45 -    (by Markus Wenzel).
    1.46 + * New command to find all rules whose conclusion matches the current goal.
    1.47  
    1.48 -  * Pure/HOL: infrastructure for generating functional and relational
    1.49 -    code, using the ML run-time environment
    1.50 -    (by Stefan Berghofer).
    1.51 + * New command to trace why unification failed.
    1.52  
    1.53 -  * HOL/library: numerals on all number types; several improvements of
    1.54 -    tuple and record types; new definite description operator; keep
    1.55 -    Hilbert's epsilon (Axiom of Choice) out of basic theories
    1.56 -    (by Stefan Berghofer, Larry Paulson, Markus Wenzel).
    1.57 -
    1.58 -  * HOL/Bali: large application concerning formal treatment of Java.
    1.59 -    (by David von Oheimb and Norbert Schirmer).
    1.60 + * Locales (named proof contexts).  The new implementation is fully
    1.61 +   integrated with Isar's notion of proof context, and locale specifications
    1.62 +   produce predicate definitions that allow to work with locales in more
    1.63 +   flexible ways. (Wenzel)
    1.64  
    1.65 -  * HOL/HoareParallel: large application concerning verification of
    1.66 -    parallel imperative programs (Owicki-Gries method, Rely-Guarantee
    1.67 -    method, examples of garbage collection, mutual exclusion)
    1.68 -    (by Leonor Prensa Nieto).
    1.69 -
    1.70 -  * HOL/GroupTheory: group theory examples including Sylow's theorem
    1.71 -    (by Florian Kammueller).
    1.72 + * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
    1.73 +   algebraic developments in HOL.  Currently covers group and ring theory.
    1.74 +   (Ballarin, Kammüller, Paulson)
    1.75  
    1.76 -  * HOL/IMP: several new proofs in Isar format
    1.77 -    (by Gerwin Klein).
    1.78 -
    1.79 -  * HOL/MicroJava: exception handling on the bytecode level
    1.80 -    (by Gerwin Klein).
    1.81 -
    1.82 -  * ZF/UNITY: typeless version of Chandy and Misra's formalism
    1.83 -    (by Sidi O Ehmety).
    1.84 + * HOL/Complex defines the type "complex" of the complex numbers, with numeric
    1.85 +   constants and some complex analysis, including nonstandard analysis.  The
    1.86 +   image HOL-Complex should be used for developments involving the real
    1.87 +   numbers too.  Gauge integration and hyperreal logarithms have recently
    1.88 +   been added. (Fleuriot)
    1.89  
    1.90 -  * System: improvements and simplifications of document preparation
    1.91 -    (by Markus Wenzel).
    1.92 + * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
    1.93 +   Gray and Kramer)
    1.94  
    1.95 -  * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting
    1.96 -    larger heap size of applications; support for MacOS X (Poly/ML and
    1.97 -    SML/NJ).
    1.98 + * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
    1.99 +   of choice is mechanized using Isabelle/ZF, following, Kunen's famous
   1.100 +   textbook "Set Theory". (Paulson)
   1.101  
   1.102 -You may get Isabelle2002 from any of the following mirror sites:
   1.103 +You may get Isabelle2003 from any of the following mirror sites:
   1.104  
   1.105    Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
   1.106    Munich (Germany)  http://isabelle.in.tum.de/dist/
   1.107 -  New Jersey (USA)  ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html