diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/UNITY/Detects.thy
--- a/src/HOL/UNITY/Detects.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/Detects.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,10 +9,10 @@
 
 theory Detects imports FP SubstAx begin
 
-definition Detects :: "['a set, 'a set] => 'a program set"  (infixl "Detects" 60)
+definition Detects :: "['a set, 'a set] => 'a program set"  (infixl \<open>Detects\<close> 60)
   where "A Detects B = (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
 
-definition Equality :: "['a set, 'a set] => 'a set"  (infixl "<==>" 60)
+definition Equality :: "['a set, 'a set] => 'a set"  (infixl \<open><==>\<close> 60)
   where "A <==> B = (-A \<union> B) \<inter> (A \<union> -B)"