src/HOL/Hyperreal/MacLaurin.thy
changeset 15944 9b00875e21f7
parent 15561 045a07ac35a7
child 16775 c1b87ef4a1c3
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:02:45 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon May 09 16:38:56 2005 +0200
     1.3 @@ -1,10 +1,11 @@
     1.4 -(*  Title       : MacLaurin.thy
     1.5 +(*  ID          : $Id$
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 2001 University of Edinburgh
     1.8 -    Description : MacLaurin series
     1.9      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    1.10  *)
    1.11  
    1.12 +header{*MacLaurin Series*}
    1.13 +
    1.14  theory MacLaurin
    1.15  imports Log
    1.16  begin
    1.17 @@ -583,7 +584,7 @@
    1.18        in Maclaurin_all_le_objl)
    1.19      apply safe
    1.20      apply simp
    1.21 -    apply (simplesubst mod_Suc_eq_Suc_mod)  --{*simultaneous substitution*}
    1.22 +    apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
    1.23      apply (cut_tac m=m in mod_exhaust_less_4, safe, simp+)
    1.24      apply (rule DERIV_minus, simp+)
    1.25      apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)