src/HOL/Transcendental.thy
 changeset 56217 dc429a5b13c4 parent 56213 e5720d3c18f0 child 56261 918432e3fcfa
```     1.1 --- a/src/HOL/Transcendental.thy	Wed Mar 19 14:55:47 2014 +0000
1.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 19 17:06:02 2014 +0000
1.3 @@ -2396,15 +2396,6 @@
1.4    thus ?thesis unfolding cos_coeff_def by (simp add: mult_ac)
1.5  qed
1.6
1.7 -lemma real_mult_inverse_cancel:
1.8 -     "[|(0::real) < x; 0 < x1; x1 * y < x * u |]
1.9 -      ==> inverse x * y < inverse x1 * u"
1.10 -  by (metis field_divide_inverse mult_commute mult_assoc pos_divide_less_eq pos_less_divide_eq)
1.11 -
1.12 -lemma real_mult_inverse_cancel2:
1.13 -     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
1.14 -  by (auto dest: real_mult_inverse_cancel simp add: mult_ac)
1.15 -
1.16  lemmas realpow_num_eq_if = power_eq_if
1.17
1.18  lemma sumr_pos_lt_pair:
1.19 @@ -3208,7 +3199,7 @@
1.20
1.21  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
1.22    apply (rule power_inverse [THEN subst])
1.23 -  apply (rule_tac c1 = "(cos x)\<^sup>2" in real_mult_right_cancel [THEN iffD1])
1.24 +  apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
1.25    apply (auto dest: field_power_not_zero
1.26            simp add: power_mult_distrib distrib_right power_divide tan_def
1.27                      mult_assoc power_inverse [symmetric])
```