# HG changeset patch
# User nipkow
# Date 1052757741 -7200
# Node ID 24bf519625abb98e196eb5fc00189aa23a8a8736
# Parent  5fc9474833e563a6ec5e70905923a5c9e331c4a9
*** empty log message ***

diff -r 5fc9474833e5 -r 24bf519625ab ANNOUNCE
--- 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