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/Rings.thy
changeset 36977 71c8973a604b
parent 36970 fb3fdb4b585e
child 37767 a2b7a20d6ea3 
--- a/src/HOL/Rings.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Rings.thy	Mon May 17 18:59:59 2010 -0700
@@ -956,7 +956,7 @@
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
     by (auto simp add: abs_if not_less)
     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
-     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
+     auto intro!: less_imp_le add_neg_neg)
 qed (auto simp add: abs_if)
 
 lemma zero_le_square [simp]: "0 \<le> a * a"
isabelle