src/HOL/Nat_Numeral.thy

--- a/src/HOL/Nat_Numeral.thy	Sat Aug 20 07:09:44 2011 -0700
+++ b/src/HOL/Nat_Numeral.thy	Sat Aug 20 09:59:28 2011 -0700
@@ -129,6 +129,14 @@
 
 end
 
+context idom
+begin
+
+lemma power2_eq_iff: "x\<twosuperior> = y\<twosuperior> \<longleftrightarrow> x = y \<or> x = - y"
+  unfolding power2_eq_square by (rule square_eq_iff)
+
+end
+
 context linordered_ring
 begin