# HG changeset patch
# User huffman
# Date 1274111146 25200
# Node ID fb3fdb4b585e9ee90a9d9f6e9bcfa34887e939e9
# Parent  a354605f03dc5fab7f49b67aef7b316c0822b19c
remove simp attribute from square_eq_1_iff

diff -r a354605f03dc -r fb3fdb4b585e src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon May 17 08:40:17 2010 -0700
+++ b/src/HOL/Rings.thy	Mon May 17 08:45:46 2010 -0700
@@ -349,7 +349,7 @@
 class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
 begin
 
-lemma square_eq_1_iff [simp]:
+lemma square_eq_1_iff:
   "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
 proof -
   have "(x - 1) * (x + 1) = x * x - 1"
diff -r a354605f03dc -r fb3fdb4b585e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon May 17 08:40:17 2010 -0700
+++ b/src/HOL/Transcendental.thy	Mon May 17 08:45:46 2010 -0700
@@ -1778,7 +1778,7 @@
 lemma sin_pi_half [simp]: "sin(pi/2) = 1"
 apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
 apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
-apply (simp add: power2_eq_square)
+apply (simp add: power2_eq_1_iff)
 done
 
 lemma cos_pi [simp]: "cos pi = -1"