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.
more "anti_sym" -> "antisym" (cf. a4179bf442d1);
authorwenzelm
Fri, 13 Nov 2009 15:38:45 +0100
changeset 33659 2d7ab9458518
parent 33658 eb8b9c8a3662
child 33665 bdcabcffaaf6
more "anti_sym" -> "antisym" (cf. a4179bf442d1);
src/HOL/Deriv.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Deriv.thy	Fri Nov 13 14:14:16 2009 +0100
+++ b/src/HOL/Deriv.thy	Fri Nov 13 15:38:45 2009 +0100
@@ -1267,7 +1267,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 real_le_anti_sym real_le_linear
+    by (metis diff_self le_eqI le_iff_diff_le_0 real_le_antisym real_le_linear
               split_mult_pos_le)
   with prems show False
     by (metis DERIV_unique order_less_imp_le)
isabelle