src/HOL/Modules.thy

 lemma module_hom_scale: "module_hom s1 s2 f \<Longrightarrow> module_hom s1 s2 (\<lambda>x. s2 c (f x))"
   by (simp add: module_hom_iff module.scale_scale module.scale_right_distrib ac_simps)
 
 lemma module_hom_compose_scale:
   "module_hom s1 s2 (\<lambda>x. s2 (f x) (c))"
-  if "module_hom s1 ( *) f"
-proof -
-  interpret mh: module_hom s1 "( *)" f by fact
+  if "module_hom s1 (*) f"
+proof -
+  interpret mh: module_hom s1 "(*)" f by fact
   show ?thesis
     by unfold_locales (simp_all add: mh.add mh.scale m2.scale_left_distrib)
 qed
 
 lemma bij_module_hom_imp_inv_module_hom: "module_hom scale1 scale2 f \<Longrightarrow> bij f \<Longrightarrow>

 lemma module_hom_scale_self[simp]:
   "module_hom scale scale (\<lambda>x. scale c x)"
   using module_axioms module_hom_iff scale_left_commute scale_right_distrib by blast
 
 lemma module_hom_scale_left[simp]:
-  "module_hom ( *) scale (\<lambda>r. scale r x)"
+  "module_hom (*) scale (\<lambda>r. scale r x)"
   by unfold_locales (auto simp: algebra_simps)
 
 lemma module_hom_id: "module_hom scale scale id"
   by (simp add: module_hom_iff module_axioms)