# HG changeset patch
# User huffman
# Date 1313869875 25200
# Node ID 0e19dcf19c61e85a2d04f4b579dca50271fee1ed
# Parent  00dd3c4dabe083a91a8475320f87db223dc5ed45
remove redundant lemma realpow_two_disj, use square_eq_iff or power2_eq_iff instead

diff -r 00dd3c4dabe0 -r 0e19dcf19c61 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Aug 20 10:08:47 2011 -0700
+++ b/src/HOL/RealDef.thy	Sat Aug 20 12:51:15 2011 -0700
@@ -1618,13 +1618,6 @@
   shows "x + y = 0 \<longleftrightarrow> y = - x"
 by (auto dest: minus_unique)
 
-text {* TODO: no longer real-specific; rename and move elsewhere *}
-lemma realpow_two_disj:
-  fixes x :: "'a::idom"
-  shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-using realpow_two_diff [of x y]
-by (auto simp add: add_eq_0_iff)
-
 text {* FIXME: declare this [simp] for all types, or not at all *}
 lemma real_two_squares_add_zero_iff [simp]:
   "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"