1.1 --- a/src/HOL/Ln.thy	Fri Nov 13 11:34:05 2009 +0000
     1.2 +++ b/src/HOL/Ln.thy	Fri Nov 13 17:15:12 2009 +0000
     1.3 @@ -342,9 +342,6 @@
     1.4    apply auto
     1.5  done
     1.6  
     1.7 -lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
     1.8 -  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
     1.9 -
    1.10  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
    1.11  proof -
    1.12    assume "exp 1 <= x" and "x <= y"

     2.1 --- a/src/HOL/Transcendental.thy	Fri Nov 13 11:34:05 2009 +0000
     2.2 +++ b/src/HOL/Transcendental.thy	Fri Nov 13 17:15:12 2009 +0000
     2.3 @@ -1213,6 +1213,9 @@
     2.4  apply (simp_all add: abs_if isCont_ln)
     2.5  done
     2.6  
     2.7 +lemma DERIV_ln_divide: "0 < x ==> DERIV ln x :> 1 / x"
     2.8 +  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
     2.9 +
    2.10  lemma ln_series: assumes "0 < x" and "x < 2"
    2.11    shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))" (is "ln x = suminf (?f (x - 1))")
    2.12  proof -
    2.13 @@ -1702,9 +1705,8 @@
    2.14  apply (drule_tac f = cos in Rolle)
    2.15  apply (drule_tac [5] f = cos in Rolle)
    2.16  apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
    2.17 -apply (drule_tac y1 = xa in order_le_less_trans [THEN sin_gt_zero])
    2.18 -apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
    2.19 -apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
    2.20 +apply (metis order_less_le_trans real_less_def sin_gt_zero)
    2.21 +apply (metis order_less_le_trans real_less_def sin_gt_zero)
    2.22  done
    2.23  
    2.24  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    2.25 @@ -2436,14 +2438,8 @@
    2.26  apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
    2.27  apply (subgoal_tac "isCont arctan (tan (arctan x))", simp)
    2.28  apply (erule (1) isCont_inverse_function2 [where f=tan])
    2.29 -apply (clarify, rule arctan_tan)
    2.30 -apply (erule (1) order_less_le_trans)
    2.31 -apply (erule (1) order_le_less_trans)
    2.32 -apply (clarify, rule isCont_tan)
    2.33 -apply (rule less_imp_neq [symmetric])
    2.34 -apply (rule cos_gt_zero_pi)
    2.35 -apply (erule (1) order_less_le_trans)
    2.36 -apply (erule (1) order_le_less_trans)
    2.37 +apply (metis arctan_tan order_le_less_trans order_less_le_trans)
    2.38 +apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans real_less_def)
    2.39  done
    2.40  
    2.41  lemma DERIV_arcsin:
    2.42 @@ -3119,8 +3115,7 @@
    2.43  lemma polar_ex2:
    2.44       "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
    2.45  apply (insert polar_ex1 [where x=x and y="-y"], simp, clarify)
    2.46 -apply (rule_tac x = r in exI)
    2.47 -apply (rule_tac x = "-a" in exI, simp)
    2.48 +apply (metis cos_minus minus_minus minus_mult_right sin_minus)
    2.49  done
    2.50  
    2.51  lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"