# HG changeset patch
# User wenzelm
# Date 1246548654 -7200
# Node ID 7c35d9ad0349037165630442962711becd63bccf
# Parent  1a7ade46061b8a02c87de7ccf0a9fcd9e073500e
misc tuning;

diff -r 1a7ade46061b -r 7c35d9ad0349 NEWS
--- a/NEWS	Thu Jul 02 15:37:22 2009 +0200
+++ b/NEWS	Thu Jul 02 17:30:54 2009 +0200
@@ -37,11 +37,13 @@
 * New method "linarith" invokes existing linear arithmetic decision
 procedure only.
 
-* Implementation of quickcheck using generic code generator; default generators
-are provided for all suitable HOL types, records and datatypes.
-
-* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
-Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
+* Implementation of quickcheck using generic code generator; default
+generators are provided for all suitable HOL types, records and
+datatypes.
+
+* Constants Set.Pow and Set.image now with authentic syntax;
+object-logic definitions Set.Pow_def and Set.image_def.
+INCOMPATIBILITY.
 
 * Renamed theorems:
 Suc_eq_add_numeral_1 -> Suc_eq_plus1
@@ -49,10 +51,12 @@
 Suc_plus1 -> Suc_eq_plus1
 
 * New sledgehammer option "Full Types" in Proof General settings menu.
-Causes full type information to be output to the ATPs. This slows ATPs down
-considerably but eliminates a source of unsound "proofs" that fail later.
-
-* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
+Causes full type information to be output to the ATPs.  This slows
+ATPs down considerably but eliminates a source of unsound "proofs"
+that fail later.
+
+* Discontinued ancient tradition to suffix certain ML module names
+with "_package", e.g.:
 
     DatatypePackage ~> Datatype
     InductivePackage ~> Inductive
@@ -61,28 +65,30 @@
 
 INCOMPATIBILITY.
 
-* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
-If possible, use NewNumberTheory, not NumberTheory.
+* NewNumberTheory: Jeremy Avigad's new version of part of
+NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
 
 * Simplified interfaces of datatype module.  INCOMPATIBILITY.
 
-* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
-INCOMPATIBILITY.
-
-* New evaluator "approximate" approximates an real valued term using the same method as the
-approximation method. 
-
-* "approximate" supports now arithmetic expressions as boundaries of intervals and implements
-interval splitting and taylor series expansion.
-
-* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in 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.
-
-* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
-(auto intro!: DERIV_intros)
-INCOMPATIBILITY.
+* Abbreviation "arbitrary" of "undefined" has disappeared; use
+"undefined" directly.  INCOMPATIBILITY.
+
+* New evaluator "approximate" approximates an real valued term using
+the same method as the approximation method.
+
+* Method "approximate" supports now arithmetic expressions as
+boundaries of intervals and implements interval splitting and Taylor
+series expansion.
+
+* Changed DERIV_intros to a dynamic fact (via NamedThmsFun).  Each of
+the theorems in 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.
+
+* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
+replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
+
 
 *** ML ***