1.1 --- a/src/HOL/MacLaurin.thy	Thu Mar 05 00:16:28 2009 +0100
     1.2 +++ b/src/HOL/MacLaurin.thy	Wed Mar 04 17:12:23 2009 -0800
     1.3 @@ -82,13 +82,13 @@
     1.4   apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     1.5   apply (simp del: setsum_op_ivl_Suc)
     1.6   apply (insert sumr_offset4 [of "Suc 0"])
     1.7 - apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
     1.8 + apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
     1.9   apply (rule lemma_DERIV_subst)
    1.10    apply (rule DERIV_add)
    1.11     apply (rule_tac [2] DERIV_const)
    1.12    apply (rule DERIV_sumr, clarify)
    1.13    prefer 2 apply simp
    1.14 - apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc)
    1.15 + apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
    1.16   apply (rule DERIV_cmult)
    1.17   apply (rule lemma_DERIV_subst)
    1.18    apply (best intro: DERIV_chain2 intro!: DERIV_intros)
    1.19 @@ -145,7 +145,7 @@
    1.20      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.21      apply (simp del: setsum_op_ivl_Suc)
    1.22      apply (insert sumr_offset4 [of "Suc 0"])
    1.23 -    apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    1.24 +    apply (simp del: setsum_op_ivl_Suc fact_Suc)
    1.25      done
    1.26  
    1.27    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    1.28 @@ -205,7 +205,7 @@
    1.29        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
    1.30        diff n t / real (fact n) * h ^ n"
    1.31        using `difg (Suc m) t = 0`
    1.32 -      by (simp add: m f_h difg_def del: realpow_Suc fact_Suc)
    1.33 +      by (simp add: m f_h difg_def del: fact_Suc)
    1.34    qed
    1.35  
    1.36  qed