misc tuning;
authorwenzelm
Thu Jul 02 17:30:54 2009 +0200 (2009-07-02)
changeset 319007c35d9ad0349
parent 31899 1a7ade46061b
child 31901 e280491f36b8
misc tuning;
NEWS
     1.1 --- a/NEWS	Thu Jul 02 15:37:22 2009 +0200
     1.2 +++ b/NEWS	Thu Jul 02 17:30:54 2009 +0200
     1.3 @@ -37,11 +37,13 @@
     1.4  * New method "linarith" invokes existing linear arithmetic decision
     1.5  procedure only.
     1.6  
     1.7 -* Implementation of quickcheck using generic code generator; default generators
     1.8 -are provided for all suitable HOL types, records and datatypes.
     1.9 -
    1.10 -* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
    1.11 -Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
    1.12 +* Implementation of quickcheck using generic code generator; default
    1.13 +generators are provided for all suitable HOL types, records and
    1.14 +datatypes.
    1.15 +
    1.16 +* Constants Set.Pow and Set.image now with authentic syntax;
    1.17 +object-logic definitions Set.Pow_def and Set.image_def.
    1.18 +INCOMPATIBILITY.
    1.19  
    1.20  * Renamed theorems:
    1.21  Suc_eq_add_numeral_1 -> Suc_eq_plus1
    1.22 @@ -49,10 +51,12 @@
    1.23  Suc_plus1 -> Suc_eq_plus1
    1.24  
    1.25  * New sledgehammer option "Full Types" in Proof General settings menu.
    1.26 -Causes full type information to be output to the ATPs. This slows ATPs down
    1.27 -considerably but eliminates a source of unsound "proofs" that fail later.
    1.28 -
    1.29 -* Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
    1.30 +Causes full type information to be output to the ATPs.  This slows
    1.31 +ATPs down considerably but eliminates a source of unsound "proofs"
    1.32 +that fail later.
    1.33 +
    1.34 +* Discontinued ancient tradition to suffix certain ML module names
    1.35 +with "_package", e.g.:
    1.36  
    1.37      DatatypePackage ~> Datatype
    1.38      InductivePackage ~> Inductive
    1.39 @@ -61,28 +65,30 @@
    1.40  
    1.41  INCOMPATIBILITY.
    1.42  
    1.43 -* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory.
    1.44 -If possible, use NewNumberTheory, not NumberTheory.
    1.45 +* NewNumberTheory: Jeremy Avigad's new version of part of
    1.46 +NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
    1.47  
    1.48  * Simplified interfaces of datatype module.  INCOMPATIBILITY.
    1.49  
    1.50 -* Abbreviation "arbitrary" of "undefined" has disappeared; use "undefined" directly.
    1.51 -INCOMPATIBILITY.
    1.52 -
    1.53 -* New evaluator "approximate" approximates an real valued term using the same method as the
    1.54 -approximation method. 
    1.55 -
    1.56 -* "approximate" supports now arithmetic expressions as boundaries of intervals and implements
    1.57 -interval splitting and taylor series expansion.
    1.58 -
    1.59 -* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
    1.60 -assumes composition with an additional function and matches a variable to the
    1.61 -derivative, which has to be solved by the simplifier. Hence
    1.62 -(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
    1.63 -
    1.64 -* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
    1.65 -(auto intro!: DERIV_intros)
    1.66 -INCOMPATIBILITY.
    1.67 +* Abbreviation "arbitrary" of "undefined" has disappeared; use
    1.68 +"undefined" directly.  INCOMPATIBILITY.
    1.69 +
    1.70 +* New evaluator "approximate" approximates an real valued term using
    1.71 +the same method as the approximation method.
    1.72 +
    1.73 +* Method "approximate" supports now arithmetic expressions as
    1.74 +boundaries of intervals and implements interval splitting and Taylor
    1.75 +series expansion.
    1.76 +
    1.77 +* Changed DERIV_intros to a dynamic fact (via NamedThmsFun).  Each of
    1.78 +the theorems in DERIV_intros assumes composition with an additional
    1.79 +function and matches a variable to the derivative, which has to be
    1.80 +solved by the simplifier.  Hence (auto intro!: DERIV_intros) computes
    1.81 +the derivative of most elementary terms.
    1.82 +
    1.83 +* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
    1.84 +replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
    1.85 +
    1.86  
    1.87  *** ML ***
    1.88