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.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
```