src/HOL/Hyperreal/MacLaurin.thy
changeset 15481 fc075ae929e4
parent 15251 bb6f072c8d10
child 15536 3ce1cb7a24f0
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -579,7 +579,7 @@
     1.4        in Maclaurin_all_le_objl)
     1.5      apply safe
     1.6      apply simp
     1.7 -    apply (subst mod_Suc_eq_Suc_mod)
     1.8 +    apply (simplesubst mod_Suc_eq_Suc_mod)  --{*simultaneous substitution*}
     1.9      apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
    1.10      apply (rule DERIV_minus, simp+)
    1.11      apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)