equal
deleted
inserted
replaced
378 apply (unfold deriv_def, unfold LIM_def, clarsimp) |
378 apply (unfold deriv_def, unfold LIM_def, clarsimp) |
379 apply (rule exI) |
379 apply (rule exI) |
380 apply (rule conjI) |
380 apply (rule conjI) |
381 prefer 2 |
381 prefer 2 |
382 apply clarsimp |
382 apply clarsimp |
383 apply (subgoal_tac "(ln (x + xa) + - ln x) / xa + - (1 / x) = |
383 apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) = |
384 (ln (1 + xa / x) - xa / x) / xa") |
384 (ln (1 + xa / x) - xa / x) / xa") |
385 apply (erule ssubst) |
385 apply (erule ssubst) |
386 apply (subst abs_divide) |
386 apply (subst abs_divide) |
387 apply (rule mult_imp_div_pos_less) |
387 apply (rule mult_imp_div_pos_less) |
388 apply force |
388 apply force |
403 apply (simp only: mult_ac) |
403 apply (simp only: mult_ac) |
404 apply (rule mult_strict_left_mono) |
404 apply (rule mult_strict_left_mono) |
405 apply (erule conjE, assumption) |
405 apply (erule conjE, assumption) |
406 apply force |
406 apply force |
407 apply simp |
407 apply simp |
408 apply (subst diff_minus [THEN sym])+ |
|
409 apply (subst ln_div [THEN sym]) |
408 apply (subst ln_div [THEN sym]) |
410 apply arith |
409 apply arith |
411 apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq |
410 apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq |
412 add_divide_distrib power2_eq_square) |
411 add_divide_distrib power2_eq_square) |
413 apply (rule mult_pos_pos, assumption)+ |
412 apply (rule mult_pos_pos, assumption)+ |