diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -18,11 +18,11 @@
 \<close>
 
 record 'a monoid =  "'a partial_object" +
-  mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
-  one     :: 'a ("\<one>\<index>")
+  mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl \<open>\<otimes>\<index>\<close> 70)
+  one     :: 'a (\<open>\<one>\<index>\<close>)
 
 definition
-  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
+  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" (\<open>inv\<index> _\<close> [81] 80)
   where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
 
 definition
@@ -353,7 +353,7 @@
 subsection \<open>Power\<close>
 
 consts
-  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "[^]\<index>" 75)
+  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr \<open>[^]\<index>\<close> 75)
 
 overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
 begin
@@ -793,7 +793,7 @@
 subsection \<open>Direct Products\<close>
 
 definition
-  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
+  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr \<open>\<times>\<times>\<close> 80) where
   "G \<times>\<times> H =
     \<lparr>carrier = carrier G \<times> carrier H,
      mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
@@ -905,7 +905,7 @@
 definition iso :: "_ => _ => ('a => 'b) set"
   where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
 
-definition is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr "\<cong>" 60)
+definition is_iso :: "_ \<Rightarrow> _ \<Rightarrow> bool" (infixr \<open>\<cong>\<close> 60)
   where "G \<cong> H = (iso G H  \<noteq> {})"
 
 definition mon where "mon G H = {f \<in> hom G H. inj_on f (carrier G)}"