src/HOL/Nat_Numeral.thy
changeset 31034 736f521ad036
parent 31014 79f0858d9d49
child 31068 f591144b0f17
     1.1 --- a/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:48 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Mon May 04 14:49:49 2009 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  lemma sum_squares_eq_zero_iff:
     1.6    "x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
     1.7 -  by (simp add: sum_nonneg_eq_zero_iff)
     1.8 +  by (simp add: add_nonneg_eq_0_iff)
     1.9  
    1.10  lemma sum_squares_le_zero_iff:
    1.11    "x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0"