Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove simp attribute from power2_eq_1_iff
authorhuffman
Mon, 17 May 2010 08:40:17 -0700
changeset 36964 a354605f03dc
parent 36963 9a017146675f
child 36969 58484df8302a
child 36970 fb3fdb4b585e
remove simp attribute from power2_eq_1_iff
src/HOL/Nat_Numeral.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle