summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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: