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