--- 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 ***