1.1 --- a/src/HOL/MacLaurin.thy	Fri Jul 17 10:07:15 2009 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Fri Jul 17 13:12:18 2009 -0400
     1.3 @@ -58,17 +58,17 @@
     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_nat power_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_nat power_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_intros)
    1.19 - apply (subst fact_Suc_nat)
    1.20 + apply (subst fact_Suc)
    1.21   apply (subst real_of_nat_mult)
    1.22   apply (simp add: mult_ac)
    1.23  done
    1.24 @@ -120,7 +120,7 @@
    1.25      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    1.26      apply (simp del: setsum_op_ivl_Suc)
    1.27      apply (insert sumr_offset4 [of "Suc 0"])
    1.28 -    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
    1.29 +    apply (simp del: setsum_op_ivl_Suc fact_Suc)
    1.30      done
    1.31  
    1.32    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    1.33 @@ -180,7 +180,7 @@
    1.34        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
    1.35        diff n t / real (fact n) * h ^ n"
    1.36        using `difg (Suc m) t = 0`
    1.37 -      by (simp add: m f_h difg_def del: fact_Suc_nat)
    1.38 +      by (simp add: m f_h difg_def del: fact_Suc)
    1.39    qed
    1.40  
    1.41  qed