--- 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)}"