--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Dec 01 14:09:10 2015 +0000
@@ -688,7 +688,7 @@
"x \<in> {a <..< b}"
"(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
then show ?thesis
- by (metis (hide_lams) assms(1) diff_less_iff(1) eq_iff_diff_eq_0
+ by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
times_divide_eq_left)
qed