src/HOL/Library/BigO.thy
changeset 57512 cc97b347b301
parent 57418 6ab1c7cb0b8d
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4    shows "c \<noteq> 0 \<Longrightarrow> f \<in> O(\<lambda>x. c * f x)"
     1.5    apply (simp add: bigo_def)
     1.6    apply (rule_tac x = "abs (inverse c)" in exI)
     1.7 -  apply (simp add: abs_mult [symmetric] mult_assoc [symmetric])
     1.8 +  apply (simp add: abs_mult [symmetric] mult.assoc [symmetric])
     1.9    done
    1.10  
    1.11  lemma bigo_const_mult4:
    1.12 @@ -517,10 +517,10 @@
    1.13    apply (simp add: func_times)
    1.14    apply (auto intro!: simp add: bigo_def elt_set_times_def func_times)
    1.15    apply (rule_tac x = "\<lambda>y. inverse c * x y" in exI)
    1.16 -  apply (simp add: mult_assoc [symmetric] abs_mult)
    1.17 +  apply (simp add: mult.assoc [symmetric] abs_mult)
    1.18    apply (rule_tac x = "abs (inverse c) * ca" in exI)
    1.19    apply (rule allI)
    1.20 -  apply (subst mult_assoc)
    1.21 +  apply (subst mult.assoc)
    1.22    apply (rule mult_left_mono)
    1.23    apply (erule spec)
    1.24    apply force
    1.25 @@ -613,7 +613,7 @@
    1.26    apply (rule_tac x = c in exI)
    1.27    apply (rule allI)+
    1.28    apply (subst abs_mult)+
    1.29 -  apply (subst mult_left_commute)
    1.30 +  apply (subst mult.left_commute)
    1.31    apply (rule mult_left_mono)
    1.32    apply (erule spec)
    1.33    apply (rule abs_ge_zero)