src/HOL/Transcendental.thy
changeset 36970 fb3fdb4b585e
parent 36842 99745a4b9cc9
child 36974 b877866b5b00
     1.1 --- a/src/HOL/Transcendental.thy	Mon May 17 08:40:17 2010 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon May 17 08:45:46 2010 -0700
     1.3 @@ -1778,7 +1778,7 @@
     1.4  lemma sin_pi_half [simp]: "sin(pi/2) = 1"
     1.5  apply (cut_tac x = "pi/2" in sin_cos_squared_add2)
     1.6  apply (cut_tac sin_gt_zero [OF pi_half_gt_zero pi_half_less_two])
     1.7 -apply (simp add: power2_eq_square)
     1.8 +apply (simp add: power2_eq_1_iff)
     1.9  done
    1.10  
    1.11  lemma cos_pi [simp]: "cos pi = -1"