author | wenzelm |

Thu Jul 02 17:30:54 2009 +0200 (2009-07-02) | |

changeset 31900 | 7c35d9ad0349 |

parent 31899 | 1a7ade46061b |

child 31901 | e280491f36b8 |

misc tuning;

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