1.1 --- a/src/HOL/Big_Operators.thy	Mon May 17 18:51:25 2010 -0700
     1.2 +++ b/src/HOL/Big_Operators.thy	Mon May 17 18:59:59 2010 -0700
     1.3 @@ -673,7 +673,7 @@
     1.4    proof induct
     1.5      case empty thus ?case by simp
     1.6    next
     1.7 -    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
     1.8 +    case (insert x A) thus ?case by auto
     1.9    qed
    1.10  next
    1.11    case False thus ?thesis by (simp add: setsum_def)

     2.1 --- a/src/HOL/Groups.thy	Mon May 17 18:51:25 2010 -0700
     2.2 +++ b/src/HOL/Groups.thy	Mon May 17 18:59:59 2010 -0700
     2.3 @@ -605,7 +605,7 @@
     2.4    then show ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma add_nonneg_nonneg:
     2.8 +lemma add_nonneg_nonneg [simp]:
     2.9    assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
    2.10  proof -
    2.11    have "0 + 0 \<le> a + b" 

     3.1 --- a/src/HOL/NSA/NSCA.thy	Mon May 17 18:51:25 2010 -0700
     3.2 +++ b/src/HOL/NSA/NSCA.thy	Mon May 17 18:59:59 2010 -0700
     3.3 @@ -279,13 +279,9 @@
     3.4    "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
     3.5  apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
     3.6  apply (simp add: hcmod_i)
     3.7 -apply (rule Infinitesimal_sqrt)
     3.8  apply (rule Infinitesimal_add)
     3.9  apply (erule Infinitesimal_hrealpow, simp)
    3.10  apply (erule Infinitesimal_hrealpow, simp)
    3.11 -apply (rule add_nonneg_nonneg)
    3.12 -apply (rule zero_le_power2)
    3.13 -apply (rule zero_le_power2)
    3.14  done
    3.15  
    3.16  lemma hcomplex_Infinitesimal_iff:

     4.1 --- a/src/HOL/Nat.thy	Mon May 17 18:51:25 2010 -0700
     4.2 +++ b/src/HOL/Nat.thy	Mon May 17 18:59:59 2010 -0700
     4.3 @@ -1294,15 +1294,11 @@
     4.4  begin
     4.5  
     4.6  lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
     4.7 -  apply (induct m, simp_all)
     4.8 -  apply (erule order_trans)
     4.9 -  apply (rule ord_le_eq_trans [OF _ add_commute])
    4.10 -  apply (rule less_add_one [THEN less_imp_le])
    4.11 -  done
    4.12 +  by (induct m) simp_all
    4.13  
    4.14  lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
    4.15    apply (induct m n rule: diff_induct, simp_all)
    4.16 -  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
    4.17 +  apply (rule add_pos_nonneg [OF zero_less_one zero_le_imp_of_nat])
    4.18    done
    4.19  
    4.20  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"

     5.1 --- a/src/HOL/RealDef.thy	Mon May 17 18:51:25 2010 -0700
     5.2 +++ b/src/HOL/RealDef.thy	Mon May 17 18:59:59 2010 -0700
     5.3 @@ -1620,14 +1620,6 @@
     5.4       "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
     5.5  by (rule sum_power2_eq_zero_iff)
     5.6  
     5.7 -text {* FIXME: declare this [simp] for all types, or not at all *}
     5.8 -lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
     5.9 -by (rule sum_power2_ge_zero)
    5.10 -
    5.11 -text {* FIXME: declare this [simp] for all types, or not at all *}
    5.12 -lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
    5.13 -by (intro add_nonneg_nonneg zero_le_power2)
    5.14 -
    5.15  lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
    5.16  by (rule_tac y = 0 in order_trans, auto)
    5.17  

     6.1 --- a/src/HOL/Rings.thy	Mon May 17 18:51:25 2010 -0700
     6.2 +++ b/src/HOL/Rings.thy	Mon May 17 18:59:59 2010 -0700
     6.3 @@ -956,7 +956,7 @@
     6.4    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
     6.5      by (auto simp add: abs_if not_less)
     6.6      (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
     6.7 -     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
     6.8 +     auto intro!: less_imp_le add_neg_neg)
     6.9  qed (auto simp add: abs_if)
    6.10  
    6.11  lemma zero_le_square [simp]: "0 \<le> a * a"