src/HOL/Library/BigO.thy

--- a/src/HOL/Library/BigO.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -489,7 +489,7 @@
   shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
   apply (simp add: bigo_def)
   apply (rule_tac x = "abs (inverse c)" in exI)
-  apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
+  apply (simp add: abs_mult [symmetric] mult.assoc [symmetric])
   done
 
 lemma bigo_const_mult4:
@@ -517,10 +517,10 @@
   apply (simp add: func_times)
   apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
   apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
-  apply (simp add: mult_assoc [symmetric] abs_mult)
+  apply (simp add: mult.assoc [symmetric] abs_mult)
   apply (rule_tac x = "abs (inverse c) * ca" in exI)
   apply (rule allI)
-  apply (subst mult_assoc)
+  apply (subst mult.assoc)
   apply (rule mult_left_mono)
   apply (erule spec)
   apply force
@@ -613,7 +613,7 @@
   apply (rule_tac x = c in exI)
   apply (rule allI)+
   apply (subst abs_mult)+
-  apply (subst mult_left_commute)
+  apply (subst mult.left_commute)
   apply (rule mult_left_mono)
   apply (erule spec)
   apply (rule abs_ge_zero)