src/HOL/Real/RealPow.thy
changeset 23096 423ad2fe9f76
parent 22970 b5910e3dec4c
child 23291 9179346e1208
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu May 24 16:52:54 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu May 24 22:55:53 2007 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4  lemma sum_squares_eq_zero_iff:
     1.5    fixes x y :: "'a::ordered_ring_strict"
     1.6    shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
     1.7 -by (simp add: sum_nonneg_eq_zero_iff zero_le_square)
     1.8 +by (simp add: sum_nonneg_eq_zero_iff)
     1.9  
    1.10  lemma sum_squares_le_zero_iff:
    1.11    fixes x y :: "'a::ordered_ring_strict"