# HG changeset patch
# User haftmann
# Date 1279563543 -7200
# Node ID d78a3cdbd615acad9ec200e9ec7b034ebe1486d3
# Parent  2ae085b07f2fb9bc14a9dac83309f5405c3ed351
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq

diff -r 2ae085b07f2f -r d78a3cdbd615 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/Deriv.thy	Mon Jul 19 20:19:03 2010 +0200
@@ -1269,7 +1269,7 @@
       and "f b - f a = (b - a) * l"
     by auto
   from prems have "~(l >= 0)"
-    by (metis diff_self diff_eq_diff_less_eq' 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)