# HG changeset patch
# User huffman
# Date 1313859568 25200
# Node ID 881c324470a24010b8563ca871dd2f229fcb4608
# Parent  49be3e7d4762309de729c41299e7ea68aee47e13
add lemma power2_eq_iff

diff -r 49be3e7d4762 -r 881c324470a2 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