diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -32,10 +32,10 @@
   | Acts:  "[| act \<in> Acts F;  s \<in> reachable F;  (s,s') \<in> act |]
             ==> s' \<in> reachable F"
 
-definition Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) where
+definition Constrains :: "['a set, 'a set] => 'a program set" (infixl \<open>Co\<close> 60) where
     "A Co B == {F. F \<in> (reachable F \<inter> A)  co  B}"
 
-definition Unless  :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) where
+definition Unless  :: "['a set, 'a set] => 'a program set" (infixl \<open>Unless\<close> 60) where
     "A Unless B == (A-B) Co (A \<union> B)"
 
 definition Stable     :: "'a set => 'a program set" where