--- a/src/HOL/Hyperreal/Ln.thy Sun Sep 17 16:44:51 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Mon Sep 18 07:48:07 2006 +0200
@@ -380,7 +380,7 @@
apply (rule conjI)
prefer 2
apply clarsimp
- apply (subgoal_tac "(ln (x + xa) + - ln x) / xa + - (1 / x) =
+ apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) =
(ln (1 + xa / x) - xa / x) / xa")
apply (erule ssubst)
apply (subst abs_divide)
@@ -405,7 +405,6 @@
apply (erule conjE, assumption)
apply force
apply simp
- apply (subst diff_minus [THEN sym])+
apply (subst ln_div [THEN sym])
apply arith
apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq