changeset 56238 | 5d147e1e18d1 |
parent 56193 | c726ecfb22b6 |
child 56381 | 0556204bc230 |
--- a/src/HOL/MacLaurin.thy Fri Mar 21 08:13:23 2014 +0100 +++ b/src/HOL/MacLaurin.thy Fri Mar 21 15:36:00 2014 +0000 @@ -270,7 +270,7 @@ show ?thesis proof (cases rule: linorder_cases) assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV - have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma) + have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (auto simp add: Maclaurin_bi_le_lemma) thus ?thesis .. next assume "x < 0"