src/ZF/UNITY/WFair.thy

   transient :: "i=>i"  where
   "transient(A) =={F \<in> program. (\<exists>act\<in>Acts(F). A<=domain(act) &
                                act``A \<subseteq> state-A) & st_set(A)}"
 
 definition
-  ensures :: "[i,i] => i"       (infixl "ensures" 60)  where
+  ensures :: "[i,i] => i"       (infixl \<open>ensures\<close> 60)  where
   "A ensures B == ((A-B) co (A \<union> B)) \<inter> transient(A-B)"
 
 consts
 
   (*LEADS-TO constant for the inductive definition*)

   monos        Pow_mono
   type_intros  Union_Pow_iff [THEN iffD2] UnionI PowI
 
 definition
   (* The Visible version of the LEADS-TO relation*)
-  leadsTo :: "[i, i] => i"       (infixl "\<longmapsto>" 60)  where
+  leadsTo :: "[i, i] => i"       (infixl \<open>\<longmapsto>\<close> 60)  where
   "A \<longmapsto> B == {F \<in> program. <A,B>:leads(state, F)}"
 
 definition
   (* wlt(F, B) is the largest set that leads to B*)
   wlt :: "[i, i] => i"  where