src/HOL/Transcendental.thy
 changeset 56544 b60d5d119489 parent 56541 0e3abadbef39 child 56571 f4635657d66f
```     1.1 --- a/src/HOL/Transcendental.thy	Fri Apr 11 23:22:00 2014 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 12 17:26:27 2014 +0200
1.3 @@ -1465,7 +1465,7 @@
1.4    also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
1.5      by (metis a b divide_right_mono exp_bound exp_ge_zero)
1.6    also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
1.9    also from a have "... <= 1 + x"
1.11    finally have "exp (x - x\<^sup>2) <= 1 + x" .
1.12 @@ -2378,7 +2378,7 @@
1.13        by (intro mult_strict_right_mono zero_less_power `0 < x`)
1.14      thus "0 < ?f n"
1.15        by (simp del: mult_Suc,
1.16 -        simp add: less_divide_eq mult_pos_pos field_simps del: mult_Suc)
1.17 +        simp add: less_divide_eq field_simps del: mult_Suc)
1.18    qed
1.19    have sums: "?f sums sin x"
1.20      by (rule sin_paired [THEN sums_group], simp)
1.21 @@ -2962,8 +2962,7 @@
1.22    hence "0 < cos z" using cos_gt_zero_pi by auto
1.23    hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
1.24    have "0 < x - y" using `y < x` by auto
1.25 -  from mult_pos_pos [OF this inv_pos]
1.26 -  have "0 < tan x - tan y" unfolding tan_diff by auto
1.27 +  with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
1.28    thus ?thesis by auto
1.29  qed
1.30
```