--- a/src/HOL/Deriv.thy Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Deriv.thy Mon Jul 19 16:09:44 2010 +0200
@@ -57,7 +57,7 @@
lemma DERIV_diff:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x - g x) x :> D - E"
-by (simp only: diff_def DERIV_add DERIV_minus)
+by (simp only: diff_minus DERIV_add DERIV_minus)
lemma DERIV_add_minus:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + - g x) x :> D + - E"
@@ -1269,7 +1269,7 @@
and "f b - f a = (b - a) * l"
by auto
from prems have "~(l >= 0)"
- by (metis diff_self le_eqI le_iff_diff_le_0 order_antisym linear
+ by (metis diff_self diff_eq_diff_less_eq' le_iff_diff_le_0 order_antisym linear
split_mult_pos_le)
with prems show False
by (metis DERIV_unique order_less_imp_le)