remove simp attribute from square_eq_1_iff
authorhuffman
Mon May 17 08:45:46 2010 -0700 (2010-05-17)
changeset 36970fb3fdb4b585e
parent 36964 a354605f03dc
child 36971 522ed38eb70a
remove simp attribute from square_eq_1_iff
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Rings.thy	Mon May 17 08:40:17 2010 -0700
     1.2 +++ b/src/HOL/Rings.thy	Mon May 17 08:45:46 2010 -0700
     1.3 @@ -349,7 +349,7 @@
     1.4  class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors
     1.5  begin
     1.6  
     1.7 -lemma square_eq_1_iff [simp]:
     1.8 +lemma square_eq_1_iff:
     1.9    "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
    1.10  proof -
    1.11    have "(x - 1) * (x + 1) = x * x - 1"
     2.1 --- a/src/HOL/Transcendental.thy	Mon May 17 08:40:17 2010 -0700
     2.2 +++ b/src/HOL/Transcendental.thy	Mon May 17 08:45:46 2010 -0700
     2.3 @@ -1778,7 +1778,7 @@
     2.4  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
     2.5  apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
     2.6  apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
     2.7 -apply (simp add: power2_eq_square)
     2.8 +apply (simp add: power2_eq_1_iff)
     2.9  done
    2.10  
    2.11  lemma cos_pi [simp]: "cos pi = -1"