src/HOL/MacLaurin.thy
changeset 31881 eba74a5790d2
parent 31148 7ba7c1f8bc22
child 31882 3578434d645d
     1.1 --- a/src/HOL/MacLaurin.thy	Tue Jun 30 18:16:22 2009 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Tue Jun 30 18:21:55 2009 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4   apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
     1.5   apply (rule DERIV_cmult)
     1.6   apply (rule lemma_DERIV_subst)
     1.7 -  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
     1.8 +  apply (best intro!: DERIV_intros)
     1.9   apply (subst fact_Suc)
    1.10   apply (subst real_of_nat_mult)
    1.11   apply (simp add: mult_ac)
    1.12 @@ -565,9 +565,7 @@
    1.13      apply (clarify)
    1.14      apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    1.15      apply (cut_tac m=m in mod_exhaust_less_4)
    1.16 -    apply (safe, simp_all)
    1.17 -    apply (rule DERIV_minus, simp)
    1.18 -    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
    1.19 +    apply (safe, auto intro!: DERIV_intros)
    1.20      done
    1.21    from Maclaurin_all_le [OF diff_0 DERIV_diff]
    1.22    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and