src/HOL/Algebra/Module.thy

--- a/src/HOL/Algebra/Module.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Algebra/Module.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,7 +12,7 @@
 subsection \<open>Definitions\<close>
 
 record ('a, 'b) module = "'b ring" +
-  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
+  smult :: "['a, 'b] => 'b" (infixl \<open>\<odot>\<index>\<close> 70)
 
 locale module = R?: cring + M?: abelian_group M for M (structure) +
   assumes smult_closed [simp, intro]: