--- a/src/HOL/Real_Vector_Spaces.thy Thu Mar 12 23:05:11 2020 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Mar 14 15:58:51 2020 +0000
@@ -277,7 +277,7 @@
by (simp add: of_real_def scaleR_left_diff_distrib)
lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
- by (simp add: of_real_def mult.commute)
+ by (simp add: of_real_def)
lemma of_real_sum[simp]: "of_real (sum f s) = (\<Sum>x\<in>s. of_real (f x))"
by (induct s rule: infinite_finite_induct) auto
@@ -1365,7 +1365,7 @@
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y"
for x y :: "'a::real_normed_div_algebra"
- by (simp add: sgn_div_norm norm_mult mult.commute)
+ by (simp add: sgn_div_norm norm_mult)
hide_fact (open) sgn_mult