nipkow@14021: Subject: Announcing Isabelle2003
wenzelm@9928: To: isabelle-users@cl.cam.ac.uk
wenzelm@9928: 
nipkow@14021: Isabelle2003 is now available.
wenzelm@12927: 
nipkow@14021: This release provides many improvements and a few substantial advances over
nipkow@14021: Isabelle2002.  The most prominent highlights of Isabelle2003 are as follows
nipkow@14021: (see the NEWS of the distribution for more details):
wenzelm@12927: 
nipkow@14021:  * New framework for extracting programs from constructive proofs in HOL.
nipkow@14021:    (Berghofer)
wenzelm@12983: 
nipkow@14021:  * Improved simplifier. The premises of a goal are completely
nipkow@14021:    interreduced, ie simplified wrt each other. (Berghofer)
wenzelm@10161: 
nipkow@14021:  * Presburger arithmetic. Method arith can deal with quantified formulae over
nipkow@14021:    nat and int, and with mod, div and dvd wrt a numeral.  (Chaieb and Nipkow)
wenzelm@12983: 
nipkow@14021:  * New command to find all rules whose conclusion matches the current goal.
wenzelm@12983: 
nipkow@14021:  * New command to trace why unification failed.
wenzelm@12983: 
nipkow@14021:  * Locales (named proof contexts).  The new implementation is fully
nipkow@14021:    integrated with Isar's notion of proof context, and locale specifications
nipkow@14021:    produce predicate definitions that allow to work with locales in more
nipkow@14021:    flexible ways. (Wenzel)
wenzelm@12983: 
nipkow@14021:  * HOL/Algebra: proofs in classical algebra.  Intended as a base for all
nipkow@14021:    algebraic developments in HOL.  Currently covers group and ring theory.
nipkow@14021:    (Ballarin, Kammüller, Paulson)
wenzelm@9928: 
nipkow@14021:  * HOL/Complex defines the type "complex" of the complex numbers, with numeric
nipkow@14021:    constants and some complex analysis, including nonstandard analysis.  The
nipkow@14021:    image HOL-Complex should be used for developments involving the real
nipkow@14021:    numbers too.  Gauge integration and hyperreal logarithms have recently
nipkow@14021:    been added. (Fleuriot)
wenzelm@10162: 
nipkow@14021:  * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad,
nipkow@14021:    Gray and Kramer)
wenzelm@12983: 
nipkow@14021:  * ZF/Constructible: Gödel's proof of the relative consistency of the axiom
paulson@14022:    of choice is mechanized using Isabelle/ZF, following Kunen's well-known
nipkow@14021:    textbook "Set Theory". (Paulson)
wenzelm@10166: 
paulson@14022: You may get Isabelle2003 from the following mirror sites:
wenzelm@9928: 
wenzelm@9928:   Cambridge (UK)    http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
wenzelm@9928:   Munich (Germany)  http://isabelle.in.tum.de/dist/
nipkow@14023: 
nipkow@14023: Gerwin Klein
nipkow@14023: Tobias Nipkow
nipkow@14023: Larry Paulson