diff -r c2f672be8522 -r 44eda2314aab src/HOL/Hyperreal/Ln.thy
--- 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