diff -r f2094906e491 -r e44d86131648 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -7,10 +7,10 @@
 
 theory ClientImpl imports AllocBase Guar begin
 
-abbreviation "ask == Var(Nil)" (* input history:  tokens requested *)
-abbreviation "giv == Var([0])" (* output history: tokens granted *)
-abbreviation "rel == Var([1])" (* input history: tokens released *)
-abbreviation "tok == Var([2])" (* the number of available tokens *)
+abbreviation "ask \<equiv> Var(Nil)" (* input history:  tokens requested *)
+abbreviation "giv \<equiv> Var([0])" (* output history: tokens granted *)
+abbreviation "rel \<equiv> Var([1])" (* input history: tokens released *)
+abbreviation "tok \<equiv> Var([2])" (* the number of available tokens *)
 
 axiomatization where
   type_assumes:
@@ -21,11 +21,11 @@
    default_val(rel) = Nil & default_val(tok) = 0"
 
 
-(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
+(*Array indexing is translated to list indexing as A[n] \<equiv> nth(n-1,A). *)
 
 definition
  (** Release some client_tokens **)
-    "client_rel_act ==
+    "client_rel_act \<equiv>
      {<s,t> \<in> state*state.
       \<exists>nrel \<in> nat. nrel = length(s`rel) &
                    t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
@@ -36,14 +36,14 @@
   (** Including t=s suppresses fairness, allowing the non-trivial part
       of the action to be ignored **)
 definition
-  "client_tok_act == {<s,t> \<in> state*state. t=s |
+  "client_tok_act \<equiv> {<s,t> \<in> state*state. t=s |
                      t = s(tok:=succ(s`tok mod NbT))}"
 
 definition
-  "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+  "client_ask_act \<equiv> {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
 
 definition
-  "client_prog ==
+  "client_prog \<equiv>
    mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil &
                        s`ask = Nil & s`rel = Nil},
                     {client_rel_act, client_tok_act, client_ask_act},
@@ -55,22 +55,22 @@
 declare type_assumes [simp] default_val_assumes [simp]
 (* This part should be automated *)
 
-lemma ask_value_type [simp,TC]: "s \<in> state ==> s`ask \<in> list(nat)"
+lemma ask_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`ask \<in> list(nat)"
 apply (unfold state_def)
 apply (drule_tac a = ask in apply_type, auto)
 done
 
-lemma giv_value_type [simp,TC]: "s \<in> state ==> s`giv \<in> list(nat)"
+lemma giv_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`giv \<in> list(nat)"
 apply (unfold state_def)
 apply (drule_tac a = giv in apply_type, auto)
 done
 
-lemma rel_value_type [simp,TC]: "s \<in> state ==> s`rel \<in> list(nat)"
+lemma rel_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`rel \<in> list(nat)"
 apply (unfold state_def)
 apply (drule_tac a = rel in apply_type, auto)
 done
 
-lemma tok_value_type [simp,TC]: "s \<in> state ==> s`tok \<in> nat"
+lemma tok_value_type [simp,TC]: "s \<in> state \<Longrightarrow> s`tok \<in> nat"
 apply (unfold state_def)
 apply (drule_tac a = tok in apply_type, auto)
 done
@@ -105,14 +105,14 @@
 
 
 lemma preserves_lift_imp_stable:
-     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
+     "G \<in> preserves(lift(ff)) \<Longrightarrow> G \<in> stable({s \<in> state. P(s`ff)})"
 apply (drule preserves_imp_stable)
 apply (simp add: lift_def)
 done
 
 lemma preserves_imp_prefix:
      "G \<in> preserves(lift(ff))
-      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
+      \<Longrightarrow> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
 by (erule preserves_lift_imp_stable)
 
 (*Safety property 1 \<in> ask, rel are increasing: (24) *)
@@ -135,8 +135,8 @@
 With no Substitution Axiom, we must prove the two invariants simultaneously. *)
 
 lemma ask_Bounded_lemma:
-"[| client_prog ok G; G \<in> program |]
-      ==> client_prog \<squnion> G \<in>
+"\<lbrakk>client_prog ok G; G \<in> program\<rbrakk>
+      \<Longrightarrow> client_prog \<squnion> G \<in>
               Always({s \<in> state. s`tok \<le> NbT}  \<inter>
                       {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
 apply (rotate_tac -1)
@@ -166,22 +166,22 @@
 by (safety, auto)
 
 lemma client_prog_Join_Stable_rel_le_giv:
-"[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
-    ==> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+"\<lbrakk>client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel))\<rbrakk>
+    \<Longrightarrow> client_prog \<squnion> G \<in> Stable({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
 apply (auto simp add: lift_def)
 done
 
 lemma client_prog_Join_Always_rel_le_giv:
-     "[| client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel)) |]
-    ==> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
+     "\<lbrakk>client_prog \<squnion> G \<in> Incr(lift(giv)); G \<in> preserves(lift(rel))\<rbrakk>
+    \<Longrightarrow> client_prog \<squnion> G  \<in> Always({s \<in> state. <s`rel, s`giv> \<in> prefix(nat)})"
 by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
 
 lemma def_act_eq:
-     "A == {<s, t> \<in> state*state. P(s, t)} ==> A={<s, t> \<in> state*state. P(s, t)}"
+     "A \<equiv> {<s, t> \<in> state*state. P(s, t)} \<Longrightarrow> A={<s, t> \<in> state*state. P(s, t)}"
 by auto
 
-lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} ==> A<=state*state"
+lemma act_subset: "A={<s,t> \<in> state*state. P(s, t)} \<Longrightarrow> A<=state*state"
 by auto
 
 lemma transient_lemma:
@@ -215,8 +215,8 @@
 done
 
 lemma induct_lemma:
-"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
-  ==> client_prog \<squnion> G \<in>
+"\<lbrakk>client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program\<rbrakk>
+  \<Longrightarrow> client_prog \<squnion> G \<in>
   {s \<in> state. s`rel = k & <k,h> \<in> strict_prefix(nat)
    & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
         \<longmapsto>w {s \<in> state. <k, s`rel> \<in> strict_prefix(nat)
@@ -244,8 +244,8 @@
 done
 
 lemma rel_progress_lemma:
-"[| client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
-  ==> client_prog \<squnion> G  \<in>
+"\<lbrakk>client_prog \<squnion> G  \<in> Incr(lift(giv)); client_prog ok G; G \<in> program\<rbrakk>
+  \<Longrightarrow> client_prog \<squnion> G  \<in>
      {s \<in> state. <s`rel, h> \<in> strict_prefix(nat)
            & <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
                       \<longmapsto>w {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
@@ -273,8 +273,8 @@
 done
 
 lemma progress_lemma:
-"[| client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program |]
- ==> client_prog \<squnion> G
+"\<lbrakk>client_prog \<squnion> G \<in> Incr(lift(giv)); client_prog ok G; G \<in> program\<rbrakk>
+ \<Longrightarrow> client_prog \<squnion> G
        \<in> {s \<in> state. <h, s`giv> \<in> prefix(nat) & h pfixGe s`ask}
          \<longmapsto>w  {s \<in> state. <h, s`rel> \<in> prefix(nat)}"
 apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI],