1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:48 2009 +0200
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:49 2009 +0200
     1.3 @@ -593,7 +593,7 @@
     1.4    from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all
     1.5    from insert.hyps Fp setsum_nonneg[OF Fp]
     1.6    have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis
     1.7 -  from sum_nonneg_eq_zero_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
     1.8 +  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
     1.9    show ?case by (simp add: h)
    1.10  qed
    1.11  

     2.1 --- a/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:48 2009 +0200
     2.2 +++ b/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:49 2009 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4  
     2.5  lemma sum_squares_eq_zero_iff:
     2.6    "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
     2.7 -  by (simp add: sum_nonneg_eq_zero_iff)
     2.8 +  by (simp add: add_nonneg_eq_0_iff)
     2.9  
    2.10  lemma sum_squares_le_zero_iff:
    2.11    "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"

     3.1 --- a/src/HOL/OrderedGroup.thy	Mon May 04 14:49:48 2009 +0200
     3.2 +++ b/src/HOL/OrderedGroup.thy	Mon May 04 14:49:49 2009 +0200
     3.3 @@ -637,27 +637,6 @@
     3.4  lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
     3.5  by (simp add: algebra_simps)
     3.6  
     3.7 -lemma sum_nonneg_eq_zero_iff:
     3.8 -  assumes x: "0 \<le> x" and y: "0 \<le> y"
     3.9 -  shows "(x + y = 0) = (x = 0 \<and> y = 0)"
    3.10 -proof -
    3.11 -  have "x + y = 0 \<Longrightarrow> x = 0"
    3.12 -  proof -
    3.13 -    from y have "x + 0 \<le> x + y" by (rule add_left_mono)
    3.14 -    also assume "x + y = 0"
    3.15 -    finally have "x \<le> 0" by simp
    3.16 -    then show "x = 0" using x by (rule antisym)
    3.17 -  qed
    3.18 -  moreover have "x + y = 0 \<Longrightarrow> y = 0"
    3.19 -  proof -
    3.20 -    from x have "0 + y \<le> x + y" by (rule add_right_mono)
    3.21 -    also assume "x + y = 0"
    3.22 -    finally have "y \<le> 0" by simp
    3.23 -    then show "y = 0" using y by (rule antisym)
    3.24 -  qed
    3.25 -  ultimately show ?thesis by auto
    3.26 -qed
    3.27 -
    3.28  text{*Legacy - use @{text algebra_simps} *}
    3.29  lemmas group_simps[noatp] = algebra_simps
    3.30