src/HOL/Real.thy

   unfolding realrel_def minus_diff_minus
   by (simp only: cauchy_minus vanishes_minus simp_thms)
 
 lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n"
   unfolding realrel_def mult_diff_mult
-  by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add
+  by (subst (4) mult.commute, simp only: cauchy_mult vanishes_add
     vanishes_mult_bounded cauchy_imp_bounded simp_thms)
 
 lift_definition inverse_real :: "real \<Rightarrow> real"
   is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))"
 proof -

     apply (simp add: C_def avg_def algebra_simps)
     done
 
   have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
     apply (simp add: divide_less_eq)
-    apply (subst mult_commute)
+    apply (subst mult.commute)
     apply (frule_tac y=y in ex_less_of_nat_mult)
     apply clarify
     apply (rule_tac x=n in exI)
     apply (erule less_trans)
     apply (rule mult_strict_right_mono)