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