--- a/src/HOL/Hyperreal/Deriv.thy Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Sun Jun 17 18:47:03 2007 +0200
@@ -236,8 +236,7 @@
show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
proof (intro exI conjI)
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
- show "\<forall>z. f z - f x = ?g z * (z-x)"
- by (simp add: nonzero_mult_divide_cancel_right')
+ show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
show "isCont ?g x" using der
by (simp add: isCont_iff DERIV_iff diff_minus
cong: LIM_equal [rule_format])
@@ -248,8 +247,7 @@
then obtain g where
"(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
thus "(DERIV f x :> l)"
- by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right'
- cong: LIM_cong)
+ by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
qed
lemma DERIV_chain':