src/HOL/Hyperreal/MacLaurin.thy
changeset 25112 98824cc791c0
parent 24998 a339b33adfaf
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -279,11 +279,11 @@
     1.4  apply (case_tac "n = 0", force)
     1.5  apply (case_tac "x = 0")
     1.6  apply (rule_tac x = 0 in exI)
     1.7 -apply (force simp add: Maclaurin_bi_le_lemma)
     1.8 -apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
     1.9 +apply (force simp add: neq0_conv Maclaurin_bi_le_lemma)
    1.10 +apply (cut_tac x = x and y = 0 in linorder_less_linear, auto simp add: neq0_conv)
    1.11  txt{*Case 1, where @{term "x < 0"}*}
    1.12  apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
    1.13 -apply (simp add: abs_if)
    1.14 +apply (simp add: abs_if neq0_conv)
    1.15  apply (rule_tac x = t in exI)
    1.16  apply (simp add: abs_if)
    1.17  txt{*Case 2, where @{term "0 < x"}*}