1.1 --- a/src/HOL/Ln.thy	Tue Jun 30 18:24:00 2009 +0200
     1.2 +++ b/src/HOL/Ln.thy	Tue Jun 30 18:25:55 2009 +0200
     1.3 @@ -343,43 +343,7 @@
     1.4  done
     1.5  
     1.6  lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
     1.7 -  apply (unfold deriv_def, unfold LIM_eq, clarsimp)
     1.8 -  apply (rule exI)
     1.9 -  apply (rule conjI)
    1.10 -  prefer 2
    1.11 -  apply clarsimp
    1.12 -  apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) = 
    1.13 -      (ln (1 + xa / x) - xa / x) / xa")
    1.14 -  apply (erule ssubst)
    1.15 -  apply (subst abs_divide)
    1.16 -  apply (rule mult_imp_div_pos_less)
    1.17 -  apply force
    1.18 -  apply (rule order_le_less_trans)
    1.19 -  apply (rule abs_ln_one_plus_x_minus_x_bound)
    1.20 -  apply (subst abs_divide)
    1.21 -  apply (subst abs_of_pos, assumption)
    1.22 -  apply (erule mult_imp_div_pos_le)
    1.23 -  apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
    1.24 -  apply force
    1.25 -  apply assumption
    1.26 -  apply (simp add: power2_eq_square mult_compare_simps)
    1.27 -  apply (rule mult_imp_div_pos_less)
    1.28 -  apply (rule mult_pos_pos, assumption, assumption)
    1.29 -  apply (subgoal_tac "xa * xa = abs xa * abs xa")
    1.30 -  apply (erule ssubst)
    1.31 -  apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
    1.32 -  apply (simp only: mult_ac)
    1.33 -  apply (rule mult_strict_left_mono)
    1.34 -  apply (erule conjE, assumption)
    1.35 -  apply force
    1.36 -  apply simp
    1.37 -  apply (subst ln_div [THEN sym])
    1.38 -  apply arith
    1.39 -  apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq 
    1.40 -    add_divide_distrib power2_eq_square)
    1.41 -  apply (rule mult_pos_pos, assumption)+
    1.42 -  apply assumption
    1.43 -done
    1.44 +  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
    1.45  
    1.46  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
    1.47  proof -