Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/RealPow.thy
changeset 23096 423ad2fe9f76
parent 22970 b5910e3dec4c
child 23291 9179346e1208 
--- a/src/HOL/Real/RealPow.thy	Thu May 24 16:52:54 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Thu May 24 22:55:53 2007 +0200
@@ -149,7 +149,7 @@
 lemma sum_squares_eq_zero_iff:
   fixes x y :: "'a::ordered_ring_strict"
   shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)"
-by (simp add: sum_nonneg_eq_zero_iff zero_le_square)
+by (simp add: sum_nonneg_eq_zero_iff)
 
 lemma sum_squares_le_zero_iff:
   fixes x y :: "'a::ordered_ring_strict"
isabelle