changeset 36964 | a354605f03dc |
parent 36841 | 02df88789641 |
child 40077 | c8a9eaaa2f59 |
--- a/src/HOL/Nat_Numeral.thy Mon May 17 10:58:58 2010 +0200 +++ b/src/HOL/Nat_Numeral.thy Mon May 17 08:40:17 2010 -0700 @@ -120,9 +120,9 @@ "a\<twosuperior> = 0 \<longleftrightarrow> a = 0" unfolding power2_eq_square by simp -lemma power2_eq_1_iff [simp]: +lemma power2_eq_1_iff: "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> a = - 1" - unfolding power2_eq_square by simp + unfolding power2_eq_square by (rule square_eq_1_iff) end