1.1 --- a/src/HOL/Library/BigO.thy	Sun Jan 18 13:58:17 2009 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Jan 28 16:29:16 2009 +0100
     1.3 @@ -349,7 +349,7 @@
     1.4    apply (drule set_plus_imp_minus)
     1.5    apply (rule set_minus_imp_plus)
     1.6    apply (drule bigo_mult3 [where g = g and j = g])
     1.7 -  apply (auto simp add: ring_simps)
     1.8 +  apply (auto simp add: algebra_simps)
     1.9    done
    1.10  
    1.11  lemma bigo_mult5: "ALL x. f x ~= 0 ==>
    1.12 @@ -799,14 +799,14 @@
    1.13    apply simp
    1.14    apply (subst abs_of_nonneg)
    1.15    apply (drule_tac x = x in spec) back
    1.16 -  apply (simp add: compare_rls)
    1.17 +  apply (simp add: algebra_simps)
    1.18    apply (subst diff_minus)+
    1.19    apply (rule add_right_mono)
    1.20    apply (erule spec)
    1.21    apply (rule order_trans) 
    1.22    prefer 2
    1.23    apply (rule abs_ge_zero)
    1.24 -  apply (simp add: compare_rls)
    1.25 +  apply (simp add: algebra_simps)
    1.26    done
    1.27  
    1.28  lemma bigo_lesso3: "f =o g +o O(h) ==>
    1.29 @@ -823,7 +823,7 @@
    1.30    apply simp
    1.31    apply (subst abs_of_nonneg)
    1.32    apply (drule_tac x = x in spec) back
    1.33 -  apply (simp add: compare_rls)
    1.34 +  apply (simp add: algebra_simps)
    1.35    apply (subst diff_minus)+
    1.36    apply (rule add_left_mono)
    1.37    apply (rule le_imp_neg_le)
    1.38 @@ -831,7 +831,7 @@
    1.39    apply (rule order_trans) 
    1.40    prefer 2
    1.41    apply (rule abs_ge_zero)
    1.42 -  apply (simp add: compare_rls)
    1.43 +  apply (simp add: algebra_simps)
    1.44    done
    1.45  
    1.46  lemma bigo_lesso4: "f <o g =o O(k::'a=>'b::ordered_field) ==>
    1.47 @@ -844,7 +844,7 @@
    1.48    apply assumption
    1.49    apply (erule bigo_lesseq2) back
    1.50    apply (rule allI)
    1.51 -  apply (auto simp add: func_plus fun_diff_def compare_rls 
    1.52 +  apply (auto simp add: func_plus fun_diff_def algebra_simps
    1.53      split: split_max abs_split)
    1.54    done
    1.55  
    1.56 @@ -856,7 +856,7 @@
    1.57    apply (rule allI)
    1.58    apply (drule_tac x = x in spec)
    1.59    apply (subgoal_tac "abs(max (f x - g x) 0) = max (f x - g x) 0")
    1.60 -  apply (clarsimp simp add: compare_rls add_ac) 
    1.61 +  apply (clarsimp simp add: algebra_simps) 
    1.62    apply (rule abs_of_nonneg)
    1.63    apply (rule le_maxI2)
    1.64    done