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