src/HOL/Hahn_Banach/Vector_Space.thy

   assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
   shows "(x + y = x + z) = (y = z)"
 proof
   from y have "y = 0 + y" by simp
   also from x y have "\<dots> = (- x + x) + y" by simp
-  also from x y have "\<dots> = - x + (x + y)" by (simp add: add_assoc)
+  also from x y have "\<dots> = - x + (x + y)" by (simp add: add.assoc)
   also assume "x + y = x + z"
-  also from x z have "- x + (x + z) = - x + x + z" by (simp add: add_assoc)
+  also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)
   also from x z have "\<dots> = z" by simp
   finally show "y = z" .
 next
   assume "y = z"
   then show "x + y = x + z" by (simp only:)

   "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
     \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
   by (simp only: add_assoc [symmetric])
 
 lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
-  by (simp add: mult_commute mult_assoc2)
+  by (simp add: mult.commute mult_assoc2)
 
 lemma mult_zero_uniq:
   assumes x: "x \<in> V"  "x \<noteq> 0" and ax: "a \<cdot> x = 0"
   shows "a = 0"
 proof (rule classical)