--- a/src/HOL/Quotient.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Quotient.thy Mon Sep 23 13:32:38 2024 +0200
@@ -22,7 +22,7 @@
text \<open>Composition of Relations\<close>
abbreviation
- rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
+ rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr \<open>OOO\<close> 75)
where
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"
@@ -746,7 +746,7 @@
\<open>lift theorems to quotient types\<close>
no_notation
- rel_conj (infixr "OOO" 75)
+ rel_conj (infixr \<open>OOO\<close> 75)
section \<open>Lifting of BNFs\<close>