src/HOL/Transcendental.thy
changeset 41550 efa734d9b221
parent 38642 8fa437809c67
child 41970 47d6e13d1710
     1.1 --- a/src/HOL/Transcendental.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -164,7 +164,7 @@
     1.4    { 
     1.5      have "?s 0 = 0" by auto
     1.6      have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
     1.7 -    { fix B T E have "(if \<not> B then T else E) = (if B then E else T)" by auto } note if_eq = this
     1.8 +    have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
     1.9  
    1.10      have "?s sums y" using sums_if'[OF `f sums y`] .
    1.11      from this[unfolded sums_def, THEN LIMSEQ_Suc] 
    1.12 @@ -348,7 +348,7 @@
    1.13    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
    1.14    "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
    1.15     (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
    1.16 -by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
    1.17 +by(auto simp add: algebra_simps power_add [symmetric])
    1.18  
    1.19  lemma sumr_diff_mult_const2:
    1.20    "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
    1.21 @@ -1849,7 +1849,7 @@
    1.22  lemma sin_less_zero: 
    1.23    assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
    1.24  proof -
    1.25 -  have "0 < sin (- x)" using prems by (simp only: sin_gt_zero2) 
    1.26 +  have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2) 
    1.27    thus ?thesis by simp
    1.28  qed
    1.29  
    1.30 @@ -2107,7 +2107,7 @@
    1.31  lemma tan_less_zero: 
    1.32    assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
    1.33  proof -
    1.34 -  have "0 < tan (- x)" using prems by (simp only: tan_gt_zero) 
    1.35 +  have "0 < tan (- x)" using assms by (simp only: tan_gt_zero) 
    1.36    thus ?thesis by simp
    1.37  qed
    1.38