src/HOL/MacLaurin.thy
changeset 44890 22f665a2e91c
parent 44319 806e0390de53
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/MacLaurin.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4    (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
     1.5    diff n t / real (fact n) * h ^ n"
     1.6  proof (cases "n")
     1.7 -  case 0 with INIT1 INIT2 show ?thesis by fastsimp
     1.8 +  case 0 with INIT1 INIT2 show ?thesis by fastforce
     1.9  next
    1.10    case Suc
    1.11    hence "n > 0" by simp
    1.12 @@ -198,7 +198,7 @@
    1.13      f h =
    1.14      (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
    1.15      by (rule Maclaurin)
    1.16 -  thus ?thesis by fastsimp
    1.17 +  thus ?thesis by fastforce
    1.18  qed
    1.19  
    1.20  lemma Maclaurin2_objl: