Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
authorhaftmann
Mon, 19 Jul 2010 20:19:03 +0200
changeset 37888 d78a3cdbd615
parent 37887 2ae085b07f2f
child 37889 0d8058e0c270
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
src/HOL/Deriv.thy file | annotate | diff | comparison | revisions 
--- 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