# HG changeset patch
# User wenzelm
# Date 1259012828 -3600
# Node ID e9120a7b2779b871bddd2b95d4e2a92a33d3534d
# Parent  04c560b4ebc140cd6fe54629cd1a63ba38ac7f82
more tuning for release;

diff -r 04c560b4ebc1 -r e9120a7b2779 ANNOUNCE
--- a/ANNOUNCE	Mon Nov 23 22:35:54 2009 +0100
+++ b/ANNOUNCE	Mon Nov 23 22:47:08 2009 +0100
@@ -7,24 +7,35 @@
 file in the distribution for more details.  Some important changes
 are:
 
-* Proof method "smt" for a combination of first-order logic with equality,
-linear and nonlinear (natural/integer/real) arithmetic, and fixed-size bitvectors.
-
-* Counterexample generator tool »nitpick« based on the Kodkod relational model finder.
+* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
+on a given logic image.
 
-* Predicate compiler turning inductive into (executable) equational specifications.
-
-* Refined number theory.
-
-* Various parts of multivariate analysis.
+* HOL-SMT: proof method "smt" for a combination of first-order logic
+with equality, linear and nonlinear (natural/integer/real) arithmetic,
+and fixed-size bitvectors.
 
 * HOL-Boogie: an interactive prover back-end for Boogie and VCC.
 
+* HOL: Counterexample generator tool Nitpick based on the Kodkod
+relational model finder.
+
+* HOL: predicate compiler turning inductive into (executable)
+equational specifications.
+
+* HOL: refined number theory.
+
+* HOL: various parts of multivariate analysis.
+
+* HOLCF: new definitional domain package.
+
 * Revised tutorial on locales.
 
-* New definitional domain package for HOLCF.
+* Support for Poly/ML 5.3.0, with improved reporting of compiler
+errors and run-time exceptions, including detailed source positions.
 
-* Support for Poly/ML 5.3.0, with improved reporting of compiler errors and run-time exceptions, including detailed source positions.
+* Parallel checking of nested Isar proofs, with improved scalability
+up to 8 cores.
+
 
 You may get Isabelle2009-1 from the following mirror sites:
 
diff -r 04c560b4ebc1 -r e9120a7b2779 NEWS
--- a/NEWS	Mon Nov 23 22:35:54 2009 +0100
+++ b/NEWS	Mon Nov 23 22:47:08 2009 +0100
@@ -114,19 +114,17 @@
 fixpoint theorem.
 
 * Reorganization of number theory, INCOMPATIBILITY:
-  - new number theory development for nat and int, in
-    theories Divides and GCD as well as in new session
-    Number_Theory
-  - some constants and facts now suffixed with _nat and
-    _int accordingly
-  - former session NumberTheory now named Old_Number_Theory,
-    including theories Legacy_GCD and Primes (prefer Number_Theory
-    if possible)
+  - new number theory development for nat and int, in theories Divides
+    and GCD as well as in new session Number_Theory
+  - some constants and facts now suffixed with _nat and _int
+    accordingly
+  - former session NumberTheory now named Old_Number_Theory, including
+    theories Legacy_GCD and Primes (prefer Number_Theory if possible)
   - moved theory Pocklington from src/HOL/Library to
     src/HOL/Old_Number_Theory
 
-* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
-of finite and infinite sets. It is shown that they form a complete
+* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and
+lcm of finite and infinite sets. It is shown that they form a complete
 lattice.
 
 * Class semiring_div requires superclass no_zero_divisors and proof of
@@ -198,8 +196,6 @@
 abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
 INCOMPATIBILITY.
 
---
-
 * Most rules produced by inductive and datatype package have mandatory
 prefixes.  INCOMPATIBILITY.
 
@@ -208,8 +204,9 @@
 DERIV_intros assumes composition with an additional function and
 matches a variable to the derivative, which has to be solved by the
 Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
-of most elementary terms.  Former Maclauren.DERIV_tac and Maclauren.deriv_tac
-should be replaced by (auto intro!: DERIV_intros).  INCOMPATIBILITY.
+of most elementary terms.  Former Maclauren.DERIV_tac and
+Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros).
+INCOMPATIBILITY.
 
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold
@@ -274,7 +271,8 @@
 * The 'fixrec' package now supports "bottom patterns".  Bottom
 patterns can be used to generate strictness rules, or to make
 functions more strict (much like the bang-patterns supported by the
-Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for examples.
+Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for
+examples.
 
 
 *** ML ***