summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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