--- a/src/HOL/Hyperreal/Ln.thy Sun Jul 30 02:06:01 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Sun Jul 30 05:53:10 2006 +0200
@@ -394,7 +394,7 @@
apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
apply force
apply assumption
- apply (simp add: power2_eq_square mult_compare_simps)
+ apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
apply (rule mult_imp_div_pos_less)
apply (rule mult_pos_pos, assumption, assumption)
apply (subgoal_tac "xa * xa = abs xa * abs xa")
@@ -408,6 +408,7 @@
apply (subst diff_minus [THEN sym])+
apply (subst ln_div [THEN sym])
apply arith
+ apply assumption
apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq
add_divide_distrib power2_eq_square)
apply (rule mult_pos_pos, assumption)+