diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Examples/Coherent.thy
--- a/src/HOL/Examples/Coherent.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Examples/Coherent.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -11,9 +11,7 @@
 
 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
 
-no_notation
-  comp (infixl \<open>o\<close> 55) and
-  relcomp (infixr \<open>O\<close> 75)
+no_notation 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"