src/HOL/Limits.thy

       by (rule norm_le)
     also have "\<dots> \<le> norm (f x) * B * K"
       by (intro mult_mono' order_refl norm_g norm_ge_zero
                 mult_nonneg_nonneg K elim)
     also have "\<dots> = norm (f x) * (B * K)"
-      by (rule mult_assoc)
+      by (rule mult.assoc)
     finally show "norm (f x ** g x) \<le> norm (f x) * (B * K)" .
   qed
   with f show ?thesis
     by (rule Zfun_imp_Zfun)
 qed

   apply default
   apply (rule add_right)
   apply (rule add_left)
   apply (rule scaleR_right)
   apply (rule scaleR_left)
-  apply (subst mult_commute)
+  apply (subst mult.commute)
   using bounded by fast
 
 lemma (in bounded_bilinear) Bfun_prod_Zfun:
   assumes f: "Bfun f F"
   assumes g: "Zfun g F"

   shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
 by (simp add: LIMSEQ_iff)
 
 lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
   unfolding tendsto_def eventually_sequentially
-  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
+  by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)
 
 lemma Bseq_inverse_lemma:
   fixes x :: "'a::real_normed_div_algebra"
   shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
 apply (subst nonzero_norm_inverse, clarsimp)

   unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
 
 lemma LIM_offset_zero:
   fixes a :: "'a::real_normed_vector"
   shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
-by (drule_tac k="a" in LIM_offset, simp add: add_commute)
+by (drule_tac k="a" in LIM_offset, simp add: add.commute)
 
 lemma LIM_offset_zero_cancel:
   fixes a :: "'a::real_normed_vector"
   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
 by (drule_tac k="- a" in LIM_offset, simp)