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.7 -    by (simp add: a divide_left_mono mult_pos_pos add_pos_nonneg)
     1.8 +    by (simp add: a divide_left_mono add_pos_nonneg)
     1.9    also from a have "... <= 1 + x"
    1.10      by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
    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