# HG changeset patch # User huffman # Date 1274110817 25200 # Node ID a354605f03dc5fab7f49b67aef7b316c0822b19c # Parent 9a017146675f2bf1226fbed824a89850798c25b4 remove simp attribute from power2_eq_1_iff diff -r 9a017146675f -r a354605f03dc src/HOL/Nat_Numeral.thy --- 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\ = 0 \ a = 0" unfolding power2_eq_square by simp -lemma power2_eq_1_iff [simp]: +lemma power2_eq_1_iff: "a\ = 1 \ a = 1 \ a = - 1" - unfolding power2_eq_square by simp + unfolding power2_eq_square by (rule square_eq_1_iff) end