--- a/src/ZF/UNITY/WFair.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/WFair.thy Thu Jan 03 21:15:52 2019 +0100
@@ -21,7 +21,7 @@
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
@@ -43,7 +43,7 @@
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