merged
authorhuffman
Mon, 17 May 2010 12:00:10 -0700
changeset 36971 522ed38eb70a
parent 36970 fb3fdb4b585e (diff)
parent 36969 58484df8302a (current diff)
child 36972 aa4bc5a4be1d
child 36974 b877866b5b00
merged
--- a/src/HOL/Rings.thy	Mon May 17 17:50:09 2010 +0200
+++ b/src/HOL/Rings.thy	Mon May 17 12:00:10 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 17:50:09 2010 +0200
+++ b/src/HOL/Transcendental.thy	Mon May 17 12:00:10 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"