Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Deriv.thy
changeset 37888 d78a3cdbd615
parent 37887 2ae085b07f2f
child 37891 c26f9d06e82c 
--- 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)
isabelle