summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

ANNOUNCE

changeset 14021 | 24bf519625ab |

parent 13045 | 1db0bdda1d32 |

child 14022 | 3407f1b807ce |

--- a/ANNOUNCE Mon May 12 18:11:44 2003 +0200 +++ b/ANNOUNCE Mon May 12 18:42:21 2003 +0200 @@ -1,73 +1,48 @@ - -Subject: Announcing Isabelle2002 +Subject: Announcing Isabelle2003 To: isabelle-users@cl.cam.ac.uk -Isabelle2002 is now available. +Isabelle2003 is now available. -This release provides major improvements. The Isar language has -reached a mature state; the core engine is able to record full proof -terms; many aspects of the library have been reworked; several -substantial case studies have been added. Some changes may cause -incompatibility with earlier versions, but improve accessibility of -Isabelle for new users. +This release provides many improvements and a few substantial advances over +Isabelle2002. The most prominent highlights of Isabelle2003 are as follows +(see the NEWS of the distribution for more details): -The most prominent highlights of Isabelle2002 are as follows (see the -NEWS of the distribution for more details). - - * The Isabelle/HOL tutorial is to be published as LNCS 2283; - Isabelle2002 is the official version to go along with that book - (by Tobias Nipkow, Larry Paulson, Markus Wenzel). + * New framework for extracting programs from constructive proofs in HOL. + (Berghofer) - * Pure: explicit proof terms for all internal inferences; - object-logics, proof tools etc. will benefit automatically - (by Stefan Berghofer). + * Improved simplifier. The premises of a goal are completely + interreduced, ie simplified wrt each other. (Berghofer) - * Pure/Isar: proper integration of the locale package for modular - theory development; additional support for rename/merge - operations, and type-inference for structured specifications - (by Markus Wenzel). + * Presburger arithmetic. Method arith can deal with quantified formulae over + nat and int, and with mod, div and dvd wrt a numeral. (Chaieb and Nipkow) - * Pure/Isar: streamlined cases/induction proof patterns - (by Markus Wenzel). + * New command to find all rules whose conclusion matches the current goal. - * Pure/HOL: infrastructure for generating functional and relational - code, using the ML run-time environment - (by Stefan Berghofer). + * New command to trace why unification failed. - * HOL/library: numerals on all number types; several improvements of - tuple and record types; new definite description operator; keep - Hilbert's epsilon (Axiom of Choice) out of basic theories - (by Stefan Berghofer, Larry Paulson, Markus Wenzel). - - * HOL/Bali: large application concerning formal treatment of Java. - (by David von Oheimb and Norbert Schirmer). + * Locales (named proof contexts). The new implementation is fully + integrated with Isar's notion of proof context, and locale specifications + produce predicate definitions that allow to work with locales in more + flexible ways. (Wenzel) - * HOL/HoareParallel: large application concerning verification of - parallel imperative programs (Owicki-Gries method, Rely-Guarantee - method, examples of garbage collection, mutual exclusion) - (by Leonor Prensa Nieto). - - * HOL/GroupTheory: group theory examples including Sylow's theorem - (by Florian Kammueller). + * HOL/Algebra: proofs in classical algebra. Intended as a base for all + algebraic developments in HOL. Currently covers group and ring theory. + (Ballarin, Kammüller, Paulson) - * HOL/IMP: several new proofs in Isar format - (by Gerwin Klein). - - * HOL/MicroJava: exception handling on the bytecode level - (by Gerwin Klein). - - * ZF/UNITY: typeless version of Chandy and Misra's formalism - (by Sidi O Ehmety). + * HOL/Complex defines the type "complex" of the complex numbers, with numeric + constants and some complex analysis, including nonstandard analysis. The + image HOL-Complex should be used for developments involving the real + numbers too. Gauge integration and hyperreal logarithms have recently + been added. (Fleuriot) - * System: improvements and simplifications of document preparation - (by Markus Wenzel). + * HOL/NumberTheory: added Gauss's law of quadratic reciprocity. (Avigad, + Gray and Kramer) - * System: support for Poly/ML 4.1.1 and PolyML/4.1.2, admitting - larger heap size of applications; support for MacOS X (Poly/ML and - SML/NJ). + * ZF/Constructible: Gödel's proof of the relative consistency of the axiom + of choice is mechanized using Isabelle/ZF, following, Kunen's famous + textbook "Set Theory". (Paulson) -You may get Isabelle2002 from any of the following mirror sites: +You may get Isabelle2003 from any of the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/ Munich (Germany) http://isabelle.in.tum.de/dist/ - New Jersey (USA) ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html