1.1 --- a/src/HOL/Ln.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Ln.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -187,7 +187,7 @@
     1.4  proof -
     1.5    assume a: "0 <= (x::real)" and b: "x < 1"
     1.6    have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
     1.7 -    by (simp add: ring_simps power2_eq_square power3_eq_cube)
     1.8 +    by (simp add: algebra_simps power2_eq_square power3_eq_cube)
     1.9    also have "... <= 1"
    1.10      by (auto simp add: a)
    1.11    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    1.12 @@ -325,10 +325,10 @@
    1.13      done
    1.14    also have "... <= 2 * x^2"
    1.15      apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
    1.16 -    apply (simp add: compare_rls)
    1.17 +    apply (simp add: algebra_simps)
    1.18      apply (rule ln_one_minus_pos_lower_bound)
    1.19      apply (insert prems, auto)
    1.20 -    done 
    1.21 +    done
    1.22    finally show ?thesis .
    1.23  qed
    1.24  
    1.25 @@ -375,7 +375,7 @@
    1.26    apply simp
    1.27    apply (subst ln_div [THEN sym])
    1.28    apply arith
    1.29 -  apply (auto simp add: ring_simps add_frac_eq frac_eq_eq 
    1.30 +  apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq 
    1.31      add_divide_distrib power2_eq_square)
    1.32    apply (rule mult_pos_pos, assumption)+
    1.33    apply assumption
    1.34 @@ -394,7 +394,7 @@
    1.35      apply auto
    1.36      done
    1.37    have "x * ln y - x * ln x = x * (ln y - ln x)"
    1.38 -    by (simp add: ring_simps)
    1.39 +    by (simp add: algebra_simps)
    1.40    also have "... = x * ln(y / x)"
    1.41      apply (subst ln_div)
    1.42      apply (rule b, rule a, rule refl)