--- 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"
--- 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"