diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Examples/Coherent.thy
--- a/src/HOL/Examples/Coherent.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Examples/Coherent.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -12,8 +12,8 @@
 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
 
 no_notation
-  comp (infixl "o" 55) and
-  relcomp (infixr "O" 75)
+  comp (infixl \<open>o\<close> 55) and
+  relcomp (infixr \<open>O\<close> 75)
 
 lemma p1p2:
   assumes "col a b c l \<and> col d e f m"