# HG changeset patch
# User wenzelm
# Date 1435326944 -7200
# Node ID e0b77517f9a9b2bdc032aad46c621640a20a9159
# Parent  479071e8778f54dff4bda63842e80a43267bc1ff
more symbols;
eliminated alternative syntax;

diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Action.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -53,10 +53,10 @@
   "_SqAct"           ==   "CONST SqAct"
   "_AnAct"           ==   "CONST AnAct"
   "_Enabled"         ==   "CONST enabled"
-  "w |= [A]_v"       <=   "_SqAct A v w"
-  "w |= <A>_v"       <=   "_AnAct A v w"
-  "s |= Enabled A"   <=   "_Enabled A s"
-  "w |= unchanged f" <=   "_unchanged f w"
+  "w \<Turnstile> [A]_v"       <=   "_SqAct A v w"
+  "w \<Turnstile> <A>_v"       <=   "_AnAct A v w"
+  "s \<Turnstile> Enabled A"   <=   "_Enabled A s"
+  "w \<Turnstile> unchanged f" <=   "_unchanged f w"
 
 axiomatization where
   unl_before:    "(ACT $v) (s,t) \<equiv> v s" and
@@ -161,8 +161,8 @@
   done
 
 lemma square_simulation:
-   "\<And>f. \<lbrakk> \<turnstile> unchanged f & \<not>B \<longrightarrow> unchanged g;
-            \<turnstile> A & \<not>unchanged g \<longrightarrow> B
+   "\<And>f. \<lbrakk> \<turnstile> unchanged f \<and> \<not>B \<longrightarrow> unchanged g;
+            \<turnstile> A \<and> \<not>unchanged g \<longrightarrow> B
          \<rbrakk> \<Longrightarrow> \<turnstile> [A]_f \<longrightarrow> [B]_g"
   apply clarsimp
   apply (erule squareE)
@@ -210,29 +210,29 @@
   apply (erule maj)
   done
 
-lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F | G)"
+lemma enabled_disj1: "\<turnstile> Enabled F \<longrightarrow> Enabled (F \<or> G)"
   by (auto elim!: enabled_mono)
 
-lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F | G)"
+lemma enabled_disj2: "\<turnstile> Enabled G \<longrightarrow> Enabled (F \<or> G)"
   by (auto elim!: enabled_mono)
 
-lemma enabled_conj1: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled F"
+lemma enabled_conj1: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled F"
   by (auto elim!: enabled_mono)
 
-lemma enabled_conj2: "\<turnstile> Enabled (F & G) \<longrightarrow> Enabled G"
+lemma enabled_conj2: "\<turnstile> Enabled (F \<and> G) \<longrightarrow> Enabled G"
   by (auto elim!: enabled_mono)
 
 lemma enabled_conjE:
-    "\<lbrakk> s \<Turnstile> Enabled (F & G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
+    "\<lbrakk> s \<Turnstile> Enabled (F \<and> G); \<lbrakk> s \<Turnstile> Enabled F; s \<Turnstile> Enabled G \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
   apply (frule enabled_conj1 [action_use])
   apply (drule enabled_conj2 [action_use])
   apply simp
   done
 
-lemma enabled_disjD: "\<turnstile> Enabled (F | G) \<longrightarrow> Enabled F | Enabled G"
+lemma enabled_disjD: "\<turnstile> Enabled (F \<or> G) \<longrightarrow> Enabled F \<or> Enabled G"
   by (auto simp add: enabled_def)
 
-lemma enabled_disj: "\<turnstile> Enabled (F | G) = (Enabled F | Enabled G)"
+lemma enabled_disj: "\<turnstile> Enabled (F \<or> G) = (Enabled F \<or> Enabled G)"
   apply clarsimp
   apply (rule iffI)
    apply (erule enabled_disjD [action_use])
@@ -294,7 +294,7 @@
 
 lemma
   assumes "basevars (x,y,z)"
-  shows "\<turnstile> x \<longrightarrow> Enabled ($x & (y$ = #False))"
+  shows "\<turnstile> x \<longrightarrow> Enabled ($x \<and> (y$ = #False))"
   apply (enabled assms)
   apply auto
   done
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -5,7 +5,7 @@
 section {* A simple FIFO buffer (synchronous communication, interleaving) *}
 
 theory Buffer
-imports TLA
+imports "../TLA"
 begin
 
 consts
@@ -22,16 +22,16 @@
 defs
   BInit_def:   "BInit ic q oc    == PRED q = #[]"
   Enq_def:     "Enq ic q oc      == ACT (ic$ \<noteq> $ic)
-                                     & (q$ = $q @ [ ic$ ])
-                                     & (oc$ = $oc)"
+                                     \<and> (q$ = $q @ [ ic$ ])
+                                     \<and> (oc$ = $oc)"
   Deq_def:     "Deq ic q oc      == ACT ($q \<noteq> #[])
-                                     & (oc$ = hd< $q >)
-                                     & (q$ = tl< $q >)
-                                     & (ic$ = $ic)"
-  Next_def:    "Next ic q oc     == ACT (Enq ic q oc | Deq ic q oc)"
+                                     \<and> (oc$ = hd< $q >)
+                                     \<and> (q$ = tl< $q >)
+                                     \<and> (ic$ = $ic)"
+  Next_def:    "Next ic q oc     == ACT (Enq ic q oc \<or> Deq ic q oc)"
   IBuffer_def: "IBuffer ic q oc  == TEMP Init (BInit ic q oc)
-                                      & \<box>[Next ic q oc]_(ic,q,oc)
-                                      & WF(Deq ic q oc)_(ic,q,oc)"
+                                      \<and> \<box>[Next ic q oc]_(ic,q,oc)
+                                      \<and> WF(Deq ic q oc)_(ic,q,oc)"
   Buffer_def:  "Buffer ic oc     == TEMP (\<exists>\<exists>q. IBuffer ic q oc)"
 
 
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Buffer/DBuffer.thy
--- a/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -29,17 +29,17 @@
   (* the concatenation of the two buffers *)
   qc_def:         "PRED qc == PRED (q2 @ q1)" and
 
-  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  &  BInit mid q2 out)" and
-  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  &  unchanged (q2,out)" and
-  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  &  unchanged (inp,q1)" and
+  DBInit_def:     "DBInit   == PRED (BInit inp q1 mid  \<and>  BInit mid q2 out)" and
+  DBEnq_def:      "DBEnq    == ACT  Enq inp q1 mid  \<and>  unchanged (q2,out)" and
+  DBDeq_def:      "DBDeq    == ACT  Deq mid q2 out  \<and>  unchanged (inp,q1)" and
   DBPass_def:     "DBPass   == ACT  Deq inp q1 mid
-                                 & (q2$ = $q2 @ [ mid$ ])
-                                 & (out$ = $out)" and
-  DBNext_def:     "DBNext   == ACT  (DBEnq | DBDeq | DBPass)" and
+                                 \<and> (q2$ = $q2 @ [ mid$ ])
+                                 \<and> (out$ = $out)" and
+  DBNext_def:     "DBNext   == ACT  (DBEnq \<or> DBDeq \<or> DBPass)" and
   DBuffer_def:    "DBuffer  == TEMP Init DBInit
-                                 & \<box>[DBNext]_(inp,mid,out,q1,q2)
-                                 & WF(DBDeq)_(inp,mid,out,q1,q2)
-                                 & WF(DBPass)_(inp,mid,out,q1,q2)"
+                                 \<and> \<box>[DBNext]_(inp,mid,out,q1,q2)
+                                 \<and> WF(DBDeq)_(inp,mid,out,q1,q2)
+                                 \<and> WF(DBPass)_(inp,mid,out,q1,q2)"
 
 
 declare qc_def [simp]
@@ -109,8 +109,8 @@
 *)
 
 (* Condition (1a) *)
-lemma DBFair_1a: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
-         \<longrightarrow> (qc \<noteq> #[] & q2 = #[] \<leadsto> q2 \<noteq> #[])"
+lemma DBFair_1a: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)  
+         \<longrightarrow> (qc \<noteq> #[] \<and> q2 = #[] \<leadsto> q2 \<noteq> #[])"
   apply (rule WF1)
     apply (force simp: db_defs)
    apply (force simp: angle_def DBPass_def)
@@ -118,7 +118,7 @@
   done
 
 (* Condition (1) *)
-lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
+lemma DBFair_1: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)  
          \<longrightarrow> (Enabled (<Deq inp qc out>_(inp,qc,out)) \<leadsto> q2 \<noteq> #[])"
   apply clarsimp
   apply (rule leadsto_classical [temp_use])
@@ -130,7 +130,7 @@
   done
 
 (* Condition (2) *)
-lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBDeq)_(inp,mid,out,q1,q2)  
+lemma DBFair_2: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBDeq)_(inp,mid,out,q1,q2)  
          \<longrightarrow> (q2 \<noteq> #[] \<leadsto> DBDeq)"
   apply (rule WF_leadsto)
     apply (force simp: DBDeq_enabled [temp_use])
@@ -139,8 +139,8 @@
   done
 
 (* High-level fairness *)
-lemma DBFair: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) & WF(DBPass)_(inp,mid,out,q1,q2)  
-                                        & WF(DBDeq)_(inp,mid,out,q1,q2)   
+lemma DBFair: "\<turnstile> \<box>[DBNext]_(inp,mid,out,q1,q2) \<and> WF(DBPass)_(inp,mid,out,q1,q2)  
+                                        \<and> WF(DBDeq)_(inp,mid,out,q1,q2)   
          \<longrightarrow> WF(Deq inp qc out)_(inp,qc,out)"
   apply (auto simp del: qc_def intro!: leadsto_WF [temp_use]
     DBFair_1 [temp_use, THEN [2] LatticeTransitivity [temp_use]]
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -5,7 +5,7 @@
 section {* Lamport's "increment" example *}
 
 theory Inc
-imports TLA
+imports "../TLA"
 begin
 
 (* program counter as an enumeration type *)
@@ -45,38 +45,38 @@
   Inc_base:      "basevars (x, y, sem, pc1, pc2)" and
 
   (* definitions for high-level program *)
-  InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0" and
-  M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y" and
-  M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x" and
-  Phi_def:       "Phi     == TEMP Init InitPhi & \<box>[M1 | M2]_(x,y)
-                                 & WF(M1)_(x,y) & WF(M2)_(x,y)" and
+  InitPhi_def:   "InitPhi == PRED x = # 0 \<and> y = # 0" and
+  M1_def:        "M1      == ACT  x$ = Suc<$x> \<and> y$ = $y" and
+  M2_def:        "M2      == ACT  y$ = Suc<$y> \<and> x$ = $x" and
+  Phi_def:       "Phi     == TEMP Init InitPhi \<and> \<box>[M1 \<or> M2]_(x,y)
+                                 \<and> WF(M1)_(x,y) \<and> WF(M2)_(x,y)" and
 
   (* definitions for low-level program *)
-  InitPsi_def:   "InitPsi == PRED pc1 = #a & pc2 = #a
-                                 & x = # 0 & y = # 0 & sem = # 1" and
-  alpha1_def:    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
-                                 & unchanged(x,y,pc2)" and
-  alpha2_def:    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
-                                 & unchanged(x,y,pc1)" and
-  beta1_def:     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
-                                 & unchanged(y,sem,pc2)" and
-  beta2_def:     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
-                                 & unchanged(x,sem,pc1)" and
-  gamma1_def:    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
-                                 & unchanged(x,y,pc2)" and
-  gamma2_def:    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
-                                 & unchanged(x,y,pc1)" and
-  N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)" and
-  N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)" and
+  InitPsi_def:   "InitPsi == PRED pc1 = #a \<and> pc2 = #a
+                                 \<and> x = # 0 \<and> y = # 0 \<and> sem = # 1" and
+  alpha1_def:    "alpha1  == ACT  $pc1 = #a \<and> pc1$ = #b \<and> $sem = Suc<sem$>
+                                 \<and> unchanged(x,y,pc2)" and
+  alpha2_def:    "alpha2  == ACT  $pc2 = #a \<and> pc2$ = #b \<and> $sem = Suc<sem$>
+                                 \<and> unchanged(x,y,pc1)" and
+  beta1_def:     "beta1   == ACT  $pc1 = #b \<and> pc1$ = #g \<and> x$ = Suc<$x>
+                                 \<and> unchanged(y,sem,pc2)" and
+  beta2_def:     "beta2   == ACT  $pc2 = #b \<and> pc2$ = #g \<and> y$ = Suc<$y>
+                                 \<and> unchanged(x,sem,pc1)" and
+  gamma1_def:    "gamma1  == ACT  $pc1 = #g \<and> pc1$ = #a \<and> sem$ = Suc<$sem>
+                                 \<and> unchanged(x,y,pc2)" and
+  gamma2_def:    "gamma2  == ACT  $pc2 = #g \<and> pc2$ = #a \<and> sem$ = Suc<$sem>
+                                 \<and> unchanged(x,y,pc1)" and
+  N1_def:        "N1      == ACT  (alpha1 \<or> beta1 \<or> gamma1)" and
+  N2_def:        "N2      == ACT  (alpha2 \<or> beta2 \<or> gamma2)" and
   Psi_def:       "Psi     == TEMP Init InitPsi
-                               & \<box>[N1 | N2]_(x,y,sem,pc1,pc2)
-                               & SF(N1)_(x,y,sem,pc1,pc2)
-                               & SF(N2)_(x,y,sem,pc1,pc2)" and
+                               \<and> \<box>[N1 \<or> N2]_(x,y,sem,pc1,pc2)
+                               \<and> SF(N1)_(x,y,sem,pc1,pc2)
+                               \<and> SF(N2)_(x,y,sem,pc1,pc2)" and
 
-  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
-  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
-  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
-  PsiInv_def:   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
+  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 \<and> pc1 = #a \<and> pc2 = #a" and
+  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 \<and> pc1 = #a \<and> (pc2 = #b \<or> pc2 = #g)" and
+  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 \<and> pc2 = #a \<and> (pc1 = #b \<or> pc1 = #g)" and
+  PsiInv_def:   "PsiInv   == PRED (PsiInv1 \<or> PsiInv2 \<or> PsiInv3)"
 
 
 lemmas PsiInv_defs = PsiInv_def PsiInv1_def PsiInv2_def PsiInv3_def
@@ -89,25 +89,25 @@
 lemma PsiInv_Init: "\<turnstile> InitPsi \<longrightarrow> PsiInv"
   by (auto simp: InitPsi_def PsiInv_defs)
 
-lemma PsiInv_alpha1: "\<turnstile> alpha1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_alpha1: "\<turnstile> alpha1 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: alpha1_def PsiInv_defs)
 
-lemma PsiInv_alpha2: "\<turnstile> alpha2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_alpha2: "\<turnstile> alpha2 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: alpha2_def PsiInv_defs)
 
-lemma PsiInv_beta1: "\<turnstile> beta1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_beta1: "\<turnstile> beta1 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: beta1_def PsiInv_defs)
 
-lemma PsiInv_beta2: "\<turnstile> beta2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_beta2: "\<turnstile> beta2 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: beta2_def PsiInv_defs)
 
-lemma PsiInv_gamma1: "\<turnstile> gamma1 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_gamma1: "\<turnstile> gamma1 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: gamma1_def PsiInv_defs)
 
-lemma PsiInv_gamma2: "\<turnstile> gamma2 & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_gamma2: "\<turnstile> gamma2 \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: gamma2_def PsiInv_defs)
 
-lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) & $PsiInv \<longrightarrow> PsiInv$"
+lemma PsiInv_stutter: "\<turnstile> unchanged (x,y,sem,pc1,pc2) \<and> $PsiInv \<longrightarrow> PsiInv$"
   by (auto simp: PsiInv_defs)
 
 lemma PsiInv: "\<turnstile> Psi \<longrightarrow> \<box>PsiInv"
@@ -132,7 +132,7 @@
 lemma Init_sim: "\<turnstile> Psi \<longrightarrow> Init InitPhi"
   by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
 
-lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 | M2]_(x,y)"
+lemma Step_sim: "\<turnstile> Psi \<longrightarrow> \<box>[M1 \<or> M2]_(x,y)"
   by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
 
 
@@ -154,7 +154,7 @@
    the auxiliary lemmas are very similar.
 *)
 
-lemma Stuck_at_b: "\<turnstile> \<box>[(N1 | N2) & \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)"
+lemma Stuck_at_b: "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not> beta1]_(x,y,sem,pc1,pc2) \<longrightarrow> stable(pc1 = #b)"
   by (auto elim!: Stable squareE simp: Psi_defs)
 
 lemma N1_enabled_at_g: "\<turnstile> pc1 = #g \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
@@ -166,7 +166,7 @@
   done
 
 lemma g1_leadsto_a1:
-  "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & \<box>#True  
+  "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box>#True  
     \<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)"
   apply (rule SF1)
     apply (tactic
@@ -188,7 +188,7 @@
   done
 
 lemma g2_leadsto_a2:
-  "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
+  "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True  
     \<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)"
   apply (rule SF1)
   apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -207,7 +207,7 @@
   done
 
 lemma b2_leadsto_g2:
-  "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
+  "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True  
     \<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)"
   apply (rule SF1)
     apply (tactic
@@ -220,8 +220,8 @@
 
 (* Combine above lemmas: the second component will eventually reach pc2 = a *)
 lemma N2_leadsto_a:
-  "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & \<box>#True  
-    \<longrightarrow> (pc2 = #a | pc2 = #b | pc2 = #g \<leadsto> pc2 = #a)"
+  "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True  
+    \<longrightarrow> (pc2 = #a \<or> pc2 = #b \<or> pc2 = #g \<leadsto> pc2 = #a)"
   apply (auto intro!: LatticeDisjunctionIntro [temp_use])
     apply (rule LatticeReflexivity [temp_use])
    apply (rule LatticeTransitivity [temp_use])
@@ -230,7 +230,7 @@
 
 (* Get rid of disjunction on the left-hand side of \<leadsto> above. *)
 lemma N2_live:
-  "\<turnstile> \<box>[(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)  
+  "\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2)  
     \<longrightarrow> \<diamond>(pc2 = #a)"
   apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
   apply (case_tac "pc2 (st1 sigma)")
@@ -240,7 +240,7 @@
 (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
 
 lemma N1_enabled_at_both_a:
-  "\<turnstile> pc2 = #a & (PsiInv & pc1 = #a) \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
+  "\<turnstile> pc2 = #a \<and> (PsiInv \<and> pc1 = #a) \<longrightarrow> Enabled (<N1>_(x,y,sem,pc1,pc2))"
   apply clarsimp
   apply (rule_tac F = alpha1 in enabled_mono)
   apply (enabled Inc_base)
@@ -249,8 +249,8 @@
   done
 
 lemma a1_leadsto_b1:
-  "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))       
-         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
+  "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))       
+         \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)   
          \<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)"
   apply (rule SF1)
   apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
@@ -263,9 +263,9 @@
 
 (* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
 
-lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))              
-         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
-         \<longrightarrow> (pc1 = #b | pc1 = #g | pc1 = #a \<leadsto> pc1 = #b)"
+lemma N1_leadsto_b: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))              
+         \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)   
+         \<longrightarrow> (pc1 = #b \<or> pc1 = #g \<or> pc1 = #a \<leadsto> pc1 = #b)"
   apply (auto intro!: LatticeDisjunctionIntro [temp_use])
     apply (rule LatticeReflexivity [temp_use])
    apply (rule LatticeTransitivity [temp_use])
@@ -273,8 +273,8 @@
       simp: split_box_conj)
   done
 
-lemma N1_live: "\<turnstile> \<box>($PsiInv & [(N1 | N2) & \<not>beta1]_(x,y,sem,pc1,pc2))              
-         & SF(N1)_(x,y,sem,pc1,pc2) & \<box> SF(N2)_(x,y,sem,pc1,pc2)   
+lemma N1_live: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2))              
+         \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)   
          \<longrightarrow> \<diamond>(pc1 = #b)"
   apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
   apply (case_tac "pc1 (st1 sigma)")
@@ -291,8 +291,8 @@
 
 (* Now assemble the bits and pieces to prove that Psi is fair. *)
 
-lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))    
-         & SF(N1)_(x,y,sem,pc1,pc2) & \<box>SF(N2)_(x,y,sem,pc1,pc2)   
+lemma Fair_M1_lemma: "\<turnstile> \<box>($PsiInv \<and> [(N1 \<or> N2)]_(x,y,sem,pc1,pc2))    
+         \<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box>SF(N2)_(x,y,sem,pc1,pc2)   
          \<longrightarrow> SF(M1)_(x,y)"
   apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
    (* action premises *)
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Init.thy
--- a/src/HOL/TLA/Init.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Init.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -30,7 +30,7 @@
 translations
   "TEMP F"   => "(F::behavior \<Rightarrow> _)"
   "_Init"    == "CONST Initial"
-  "sigma |= Init F"  <= "_Init F sigma"
+  "sigma \<Turnstile> Init F"  <= "_Init F sigma"
 
 defs
   Init_def:    "sigma \<Turnstile> Init F  ==  (first_world sigma) \<Turnstile> F"
@@ -48,8 +48,8 @@
 lemma Init_simps1 [int_rewrite]:
   "\<And>F. \<turnstile> (Init \<not>F) = (\<not> Init F)"
   "\<turnstile> (Init (P \<longrightarrow> Q)) = (Init P \<longrightarrow> Init Q)"
-  "\<turnstile> (Init (P & Q)) = (Init P & Init Q)"
-  "\<turnstile> (Init (P | Q)) = (Init P | Init Q)"
+  "\<turnstile> (Init (P \<and> Q)) = (Init P \<and> Init Q)"
+  "\<turnstile> (Init (P \<or> Q)) = (Init P \<or> Init Q)"
   "\<turnstile> (Init (P = Q)) = ((Init P) = (Init Q))"
   "\<turnstile> (Init (\<forall>x. F x)) = (\<forall>x. (Init F x))"
   "\<turnstile> (Init (\<exists>x. F x)) = (\<exists>x. (Init F x))"
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -43,8 +43,8 @@
   "_constrain"  :: "[lift, type] \<Rightarrow> lift"                ("(_::_)" [4, 0] 3)
   ""            :: "lift \<Rightarrow> liftargs"                    ("_")
   "_liftargs"   :: "[lift, liftargs] \<Rightarrow> liftargs"        ("_,/ _")
-  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(|- _)" 5)
-  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ |= _)" [100,10] 10)
+  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(\<turnstile> _)" 5)
+  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
 
   (* Syntax for lifted expressions outside the scope of \<turnstile> or |= *)
   "_LIFT"       :: "lift \<Rightarrow> 'a"                          ("LIFT _")
@@ -57,11 +57,11 @@
 
   (* concrete syntax for common infix functions: reuse same symbol *)
   "_liftEqu"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ =/ _)" [50,51] 50)
-  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ ~=/ _)" [50,51] 50)
-  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("(~ _)" [40] 40)
-  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ &/ _)" [36,35] 35)
-  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                ("(_ |/ _)" [31,30] 30)
-  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ -->/ _)" [26,25] 25)
+  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<noteq>/ _)" [50,51] 50)
+  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("(\<not> _)" [40] 40)
+  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<and>/ _)" [36,35] 35)
+  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<or>/ _)" [31,30] 30)
+  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ \<longrightarrow>/ _)" [26,25] 25)
   "_liftIf"     :: "[lift, lift, lift] \<Rightarrow> lift"          ("(if (_)/ then (_)/ else (_))" 10)
   "_liftPlus"   :: "[lift, lift] \<Rightarrow> lift"                ("(_ +/ _)" [66,65] 65)
   "_liftMinus"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ -/ _)" [66,65] 65)
@@ -69,9 +69,9 @@
   "_liftDiv"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ div _)" [71,70] 70)
   "_liftMod"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ mod _)" [71,70] 70)
   "_liftLess"   :: "[lift, lift] \<Rightarrow> lift"                ("(_/ < _)"  [50, 51] 50)
-  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ <= _)" [50, 51] 50)
-  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ : _)" [50, 51] 50)
-  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ ~: _)" [50, 51] 50)
+  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
+  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
+  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)
   "_liftFinset" :: "liftargs \<Rightarrow> lift"                    ("{(_)}")
   (** TODO: syntax for lifted collection / comprehension **)
   "_liftPair"   :: "[lift,liftargs] \<Rightarrow> lift"                   ("(1'(_,/ _'))")
@@ -81,12 +81,9 @@
   "_liftList" :: "liftargs \<Rightarrow> lift"                      ("[(_)]")
 
   (* Rigid quantification (syntax level) *)
-  "_ARAll"  :: "[idts, lift] \<Rightarrow> lift"                    ("(3! _./ _)" [0, 10] 10)
-  "_AREx"   :: "[idts, lift] \<Rightarrow> lift"                    ("(3? _./ _)" [0, 10] 10)
-  "_AREx1"  :: "[idts, lift] \<Rightarrow> lift"                    ("(3?! _./ _)" [0, 10] 10)
-  "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      ("(3ALL _./ _)" [0, 10] 10)
-  "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      ("(3EX _./ _)" [0, 10] 10)
-  "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      ("(3EX! _./ _)" [0, 10] 10)
+  "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<forall>_./ _)" [0, 10] 10)
+  "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>_./ _)" [0, 10] 10)
+  "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      ("(3\<exists>!_./ _)" [0, 10] 10)
 
 translations
   "_const"        == "CONST const"
@@ -97,19 +94,16 @@
   "_RAll x A"     == "Rall x. A"
   "_REx x  A"     == "Rex x. A"
   "_REx1 x  A"    == "Rex! x. A"
-  "_ARAll"        => "_RAll"
-  "_AREx"         => "_REx"
-  "_AREx1"        => "_REx1"
 
-  "w |= A"        => "A w"
-  "LIFT A"        => "A::_=>_"
+  "w \<Turnstile> A"        => "A w"
+  "LIFT A"        => "A::_\<Rightarrow>_"
 
   "_liftEqu"      == "_lift2 (op =)"
   "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
   "_liftNot"      == "_lift (CONST Not)"
-  "_liftAnd"      == "_lift2 (op &)"
-  "_liftOr"       == "_lift2 (op | )"
-  "_liftImp"      == "_lift2 (op -->)"
+  "_liftAnd"      == "_lift2 (op \<and>)"
+  "_liftOr"       == "_lift2 (op \<or>)"
+  "_liftImp"      == "_lift2 (op \<longrightarrow>)"
   "_liftIf"       == "_lift3 (CONST If)"
   "_liftPlus"     == "_lift2 (op +)"
   "_liftMinus"    == "_lift2 (op -)"
@@ -117,8 +111,8 @@
   "_liftDiv"      == "_lift2 (op div)"
   "_liftMod"      == "_lift2 (op mod)"
   "_liftLess"     == "_lift2 (op <)"
-  "_liftLeq"      == "_lift2 (op <=)"
-  "_liftMem"      == "_lift2 (op :)"
+  "_liftLeq"      == "_lift2 (op \<le>)"
+  "_liftMem"      == "_lift2 (op \<in>)"
   "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
   "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
   "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
@@ -131,29 +125,14 @@
 
 
 
-  "w |= ~A"       <= "_liftNot A w"
-  "w |= A & B"    <= "_liftAnd A B w"
-  "w |= A | B"    <= "_liftOr A B w"
-  "w |= A --> B"  <= "_liftImp A B w"
-  "w |= u = v"    <= "_liftEqu u v w"
-  "w |= ALL x. A"   <= "_RAll x A w"
-  "w |= EX x. A"   <= "_REx x A w"
-  "w |= EX! x. A"  <= "_REx1 x A w"
-
-syntax (xsymbols)
-  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(\<turnstile> _)" 5)
-  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
-  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                (infixl "\<noteq>" 50)
-  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("\<not> _" [40] 40)
-  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<and>" 35)
-  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<or>" 30)
-  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<longrightarrow>" 25)
-  "_RAll"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>_./ _)" [0, 10] 10)
-  "_REx"        :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>_./ _)" [0, 10] 10)
-  "_REx1"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
-  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
-  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
-  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)
+  "w \<Turnstile> \<not>A"       <= "_liftNot A w"
+  "w \<Turnstile> A \<and> B"    <= "_liftAnd A B w"
+  "w \<Turnstile> A \<or> B"    <= "_liftOr A B w"
+  "w \<Turnstile> A \<longrightarrow> B"  <= "_liftImp A B w"
+  "w \<Turnstile> u = v"    <= "_liftEqu u v w"
+  "w \<Turnstile> \<forall>x. A"   <= "_RAll x A w"
+  "w \<Turnstile> \<exists>x. A"   <= "_REx x A w"
+  "w \<Turnstile> \<exists>!x. A"  <= "_REx1 x A w"
 
 defs
   Valid_def:   "\<turnstile> A    ==  \<forall>w. w \<Turnstile> A"
@@ -164,7 +143,7 @@
   unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
 
   unl_Rall:    "w \<Turnstile> \<forall>x. A x  ==  \<forall>x. (w \<Turnstile> A x)"
-  unl_Rex:     "w \<Turnstile> \<exists>x. A x   ==  \<exists> x. (w \<Turnstile> A x)"
+  unl_Rex:     "w \<Turnstile> \<exists>x. A x   ==  \<exists>x. (w \<Turnstile> A x)"
   unl_Rex1:    "w \<Turnstile> \<exists>!x. A x  ==  \<exists>!x. (w \<Turnstile> A x)"
 
 
@@ -202,15 +181,15 @@
   "\<turnstile> (#True \<longrightarrow> P) = P"  "\<turnstile> (#False \<longrightarrow> P) = #True"
   "\<turnstile> (P \<longrightarrow> #True) = #True"  "\<turnstile> (P \<longrightarrow> P) = #True"
   "\<turnstile> (P \<longrightarrow> #False) = (\<not>P)"  "\<turnstile> (P \<longrightarrow> \<not>P) = (\<not>P)"
-  "\<turnstile> (P & #True) = P"  "\<turnstile> (#True & P) = P"
-  "\<turnstile> (P & #False) = #False"  "\<turnstile> (#False & P) = #False"
-  "\<turnstile> (P & P) = P"  "\<turnstile> (P & \<not>P) = #False"  "\<turnstile> (\<not>P & P) = #False"
-  "\<turnstile> (P | #True) = #True"  "\<turnstile> (#True | P) = #True"
-  "\<turnstile> (P | #False) = P"  "\<turnstile> (#False | P) = P"
-  "\<turnstile> (P | P) = P"  "\<turnstile> (P | \<not>P) = #True"  "\<turnstile> (\<not>P | P) = #True"
+  "\<turnstile> (P \<and> #True) = P"  "\<turnstile> (#True \<and> P) = P"
+  "\<turnstile> (P \<and> #False) = #False"  "\<turnstile> (#False \<and> P) = #False"
+  "\<turnstile> (P \<and> P) = P"  "\<turnstile> (P \<and> \<not>P) = #False"  "\<turnstile> (\<not>P \<and> P) = #False"
+  "\<turnstile> (P \<or> #True) = #True"  "\<turnstile> (#True \<or> P) = #True"
+  "\<turnstile> (P \<or> #False) = P"  "\<turnstile> (#False \<or> P) = P"
+  "\<turnstile> (P \<or> P) = P"  "\<turnstile> (P \<or> \<not>P) = #True"  "\<turnstile> (\<not>P \<or> P) = #True"
   "\<turnstile> (\<forall>x. P) = P"  "\<turnstile> (\<exists>x. P) = P"
   "\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)"
-  "\<turnstile> (P|Q \<longrightarrow> R) = ((P\<longrightarrow>R)&(Q\<longrightarrow>R))"
+  "\<turnstile> (P\<or>Q \<longrightarrow> R) = ((P\<longrightarrow>R)\<and>(Q\<longrightarrow>R))"
   apply (unfold Valid_def intensional_rews)
   apply blast+
   done
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -16,50 +16,50 @@
 definition
   (* state predicates *)
   MClkInit      :: "mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> stpred"
-  where "MClkInit rcv cst p = PRED (cst!p = #clkA  &  \<not>Calling rcv p)"
+  where "MClkInit rcv cst p = PRED (cst!p = #clkA  \<and>  \<not>Calling rcv p)"
 
 definition
   (* actions *)
   MClkFwd       :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
   where "MClkFwd send rcv cst p = ACT
                            $Calling send p
-                         & $(cst!p) = #clkA
-                         & Call rcv p MClkRelayArg<arg<send!p>>
-                         & (cst!p)$ = #clkB
-                         & unchanged (rtrner send!p)"
+                         \<and> $(cst!p) = #clkA
+                         \<and> Call rcv p MClkRelayArg<arg<send!p>>
+                         \<and> (cst!p)$ = #clkB
+                         \<and> unchanged (rtrner send!p)"
 
 definition
   MClkRetry     :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
   where "MClkRetry send rcv cst p = ACT
                            $(cst!p) = #clkB
-                         & res<$(rcv!p)> = #RPCFailure
-                         & Call rcv p MClkRelayArg<arg<send!p>>
-                         & unchanged (cst!p, rtrner send!p)"
+                         \<and> res<$(rcv!p)> = #RPCFailure
+                         \<and> Call rcv p MClkRelayArg<arg<send!p>>
+                         \<and> unchanged (cst!p, rtrner send!p)"
 
 definition
   MClkReply     :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
   where "MClkReply send rcv cst p = ACT
                            \<not>$Calling rcv p
-                         & $(cst!p) = #clkB
-                         & Return send p MClkReplyVal<res<rcv!p>>
-                         & (cst!p)$ = #clkA
-                         & unchanged (caller rcv!p)"
+                         \<and> $(cst!p) = #clkB
+                         \<and> Return send p MClkReplyVal<res<rcv!p>>
+                         \<and> (cst!p)$ = #clkA
+                         \<and> unchanged (caller rcv!p)"
 
 definition
   MClkNext      :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> action"
   where "MClkNext send rcv cst p = ACT
                         (  MClkFwd send rcv cst p
-                         | MClkRetry send rcv cst p
-                         | MClkReply send rcv cst p)"
+                         \<or> MClkRetry send rcv cst p
+                         \<or> MClkReply send rcv cst p)"
 
 definition
   (* temporal *)
   MClkIPSpec    :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> PrIds \<Rightarrow> temporal"
   where "MClkIPSpec send rcv cst p = TEMP
                            Init MClkInit rcv cst p
-                         & \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
-                         & WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
-                         & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
+                         \<and> \<box>[ MClkNext send rcv cst p ]_(cst!p, rtrner send!p, caller rcv!p)
+                         \<and> WF(MClkFwd send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)
+                         \<and> SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
 
 definition
   MClkISpec     :: "mClkSndChType \<Rightarrow> mClkRcvChType \<Rightarrow> mClkStType \<Rightarrow> temporal"
@@ -73,7 +73,7 @@
 (* The Clerk engages in an action for process p only if there is an outstanding,
    unanswered call for that process.
 *)
-lemma MClkidle: "\<turnstile> \<not>$Calling send p & $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
+lemma MClkidle: "\<turnstile> \<not>$Calling send p \<and> $(cst!p) = #clkA \<longrightarrow> \<not>MClkNext send rcv cst p"
   by (auto simp: Return_def MC_action_defs)
 
 lemma MClkbusy: "\<turnstile> $Calling rcv p \<longrightarrow> \<not>MClkNext send rcv cst p"
@@ -83,7 +83,7 @@
 (* Enabledness of actions *)
 
 lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>  
-      \<turnstile> Calling send p & \<not>Calling rcv p & cst!p = #clkA   
+      \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA   
          \<longrightarrow> Enabled (MClkFwd send rcv cst p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
     @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
@@ -98,7 +98,7 @@
   by (auto simp: angle_def MClkReply_def elim: Return_changed [temp_use])
 
 lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>  
-      \<turnstile> Calling send p & \<not>Calling rcv p & cst!p = #clkB   
+      \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB   
          \<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
   apply (tactic {* action_simp_tac @{context}
     [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -55,79 +55,79 @@
   PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
 
   RdRequest_def:     "RdRequest ch p l == PRED
-                         Calling ch p & (arg<ch!p> = #(read l))"
+                         Calling ch p \<and> (arg<ch!p> = #(read l))"
   WrRequest_def:     "WrRequest ch p l v == PRED
-                         Calling ch p & (arg<ch!p> = #(write l v))"
+                         Calling ch p \<and> (arg<ch!p> = #(write l v))"
   (* a read that doesn't raise BadArg *)
   GoodRead_def:      "GoodRead mm rs p l == ACT
-                        #l : #MemLoc & ((rs!p)$ = $(mm!l))"
+                        #l \<in> #MemLoc \<and> ((rs!p)$ = $(mm!l))"
   (* a read that raises BadArg *)
   BadRead_def:       "BadRead mm rs p l == ACT
-                        #l \<notin> #MemLoc & ((rs!p)$ = #BadArg)"
+                        #l \<notin> #MemLoc \<and> ((rs!p)$ = #BadArg)"
   (* the read action with l visible *)
   ReadInner_def:     "ReadInner ch mm rs p l == ACT
                          $(RdRequest ch p l)
-                         & (GoodRead mm rs p l  |  BadRead mm rs p l)
-                         & unchanged (rtrner ch ! p)"
+                         \<and> (GoodRead mm rs p l  \<or>  BadRead mm rs p l)
+                         \<and> unchanged (rtrner ch ! p)"
   (* the read action with l quantified *)
   Read_def:          "Read ch mm rs p == ACT (\<exists>l. ReadInner ch mm rs p l)"
 
   (* similar definitions for the write action *)
   GoodWrite_def:     "GoodWrite mm rs p l v == ACT
-                        #l : #MemLoc & #v : #MemVal
-                        & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
+                        #l \<in> #MemLoc \<and> #v \<in> #MemVal
+                        \<and> ((mm!l)$ = #v) \<and> ((rs!p)$ = #OK)"
   BadWrite_def:      "BadWrite mm rs p l v == ACT
-                        \<not> (#l : #MemLoc & #v : #MemVal)
-                        & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
+                        \<not> (#l \<in> #MemLoc \<and> #v \<in> #MemVal)
+                        \<and> ((rs!p)$ = #BadArg) \<and> unchanged (mm!l)"
   WriteInner_def:    "WriteInner ch mm rs p l v == ACT
                         $(WrRequest ch p l v)
-                        & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
-                        & unchanged (rtrner ch ! p)"
+                        \<and> (GoodWrite mm rs p l v  \<or>  BadWrite mm rs p l v)
+                        \<and> unchanged (rtrner ch ! p)"
   Write_def:         "Write ch mm rs p l == ACT (\<exists>v. WriteInner ch mm rs p l v)"
 
   (* the return action *)
   MemReturn_def:     "MemReturn ch rs p == ACT
                        (   ($(rs!p) \<noteq> #NotAResult)
-                        & ((rs!p)$ = #NotAResult)
-                        & Return ch p (rs!p))"
+                        \<and> ((rs!p)$ = #NotAResult)
+                        \<and> Return ch p (rs!p))"
 
   (* the failure action of the unreliable memory *)
   MemFail_def:       "MemFail ch rs p == ACT
                         $(Calling ch p)
-                        & ((rs!p)$ = #MemFailure)
-                        & unchanged (rtrner ch ! p)"
+                        \<and> ((rs!p)$ = #MemFailure)
+                        \<and> unchanged (rtrner ch ! p)"
   (* next-state relations for reliable / unreliable memory *)
   RNext_def:         "RNext ch mm rs p == ACT
                        (  Read ch mm rs p
-                        | (\<exists>l. Write ch mm rs p l)
-                        | MemReturn ch rs p)"
+                        \<or> (\<exists>l. Write ch mm rs p l)
+                        \<or> MemReturn ch rs p)"
   UNext_def:         "UNext ch mm rs p == ACT
-                        (RNext ch mm rs p | MemFail ch rs p)"
+                        (RNext ch mm rs p \<or> MemFail ch rs p)"
 
   RPSpec_def:        "RPSpec ch mm rs p == TEMP
                         Init(PInit rs p)
-                        & \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+                        \<and> \<box>[ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
   UPSpec_def:        "UPSpec ch mm rs p == TEMP
                         Init(PInit rs p)
-                        & \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
-                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
-                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
+                        \<and> \<box>[ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
+                        \<and> WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
+                        \<and> WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
   MSpec_def:         "MSpec ch mm rs l == TEMP
                         Init(MInit mm l)
-                        & \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
+                        \<and> \<box>[ \<exists>p. Write ch mm rs p l ]_(mm!l)"
   IRSpec_def:        "IRSpec ch mm rs == TEMP
                         (\<forall>p. RPSpec ch mm rs p)
-                        & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
   IUSpec_def:        "IUSpec ch mm rs == TEMP
                         (\<forall>p. UPSpec ch mm rs p)
-                        & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l)"
+                        \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l)"
 
   RSpec_def:         "RSpec ch rs == TEMP (\<exists>\<exists>mm. IRSpec ch mm rs)"
   USpec_def:         "USpec ch == TEMP (\<exists>\<exists>mm rs. IUSpec ch mm rs)"
 
-  MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc \<longrightarrow> mm!l : #MemVal"
+  MemInv_def:        "MemInv mm l == PRED  #l \<in> #MemLoc \<longrightarrow> mm!l \<in> #MemVal"
 
 lemmas RM_action_defs =
   MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
@@ -154,7 +154,7 @@
   by (auto simp: MemInv_def intro!: necT [temp_use])
 
 lemma MemoryInvariantAll:
-    "\<turnstile> (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec ch mm rs l) \<longrightarrow> (\<forall>l. \<box>(MemInv mm l))"
+    "\<turnstile> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec ch mm rs l) \<longrightarrow> (\<forall>l. \<box>(MemInv mm l))"
   apply clarify
   apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
   done
@@ -173,7 +173,7 @@
   by (force simp: MemReturn_def angle_def)
 
 lemma MemReturn_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
-      \<turnstile> Calling ch p & (rs!p \<noteq> #NotAResult)
+      \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult)
          \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   apply (tactic
     {* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
@@ -183,32 +183,32 @@
   done
 
 lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
-      \<turnstile> Calling ch p & (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)"
+      \<turnstile> Calling ch p \<and> (arg<ch!p> = #(read l)) \<longrightarrow> Enabled (ReadInner ch mm rs p l)"
   apply (case_tac "l : MemLoc")
   apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
     intro!: exI elim!: base_enabled [temp_use])+
   done
 
 lemma WriteInner_enabled: "\<And>p. basevars (mm!l, rtrner ch ! p, rs!p) \<Longrightarrow>
-      \<turnstile> Calling ch p & (arg<ch!p> = #(write l v))
+      \<turnstile> Calling ch p \<and> (arg<ch!p> = #(write l v))
          \<longrightarrow> Enabled (WriteInner ch mm rs p l v)"
   apply (case_tac "l:MemLoc & v:MemVal")
   apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
     intro!: exI elim!: base_enabled [temp_use])+
   done
 
-lemma ReadResult: "\<turnstile> Read ch mm rs p & (\<forall>l. $(MemInv mm l)) \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
+lemma ReadResult: "\<turnstile> Read ch mm rs p \<and> (\<forall>l. $(MemInv mm l)) \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
   by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)
 
 lemma WriteResult: "\<turnstile> Write ch mm rs p l \<longrightarrow> (rs!p)` \<noteq> #NotAResult"
   by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
 
-lemma ReturnNotReadWrite: "\<turnstile> (\<forall>l. $MemInv mm l) & MemReturn ch rs p
-         \<longrightarrow> \<not> Read ch mm rs p & (\<forall>l. \<not> Write ch mm rs p l)"
+lemma ReturnNotReadWrite: "\<turnstile> (\<forall>l. $MemInv mm l) \<and> MemReturn ch rs p
+         \<longrightarrow> \<not> Read ch mm rs p \<and> (\<forall>l. \<not> Write ch mm rs p l)"
   by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
 
-lemma RWRNext_enabled: "\<turnstile> (rs!p = #NotAResult) & (!l. MemInv mm l)
-         & Enabled (Read ch mm rs p | (\<exists>l. Write ch mm rs p l))
+lemma RWRNext_enabled: "\<turnstile> (rs!p = #NotAResult) \<and> (\<forall>l. MemInv mm l)
+         \<and> Enabled (Read ch mm rs p \<or> (\<exists>l. Write ch mm rs p l))
          \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   by (force simp: RNext_def angle_def elim!: enabled_mono2
     dest: ReadResult [temp_use] WriteResult [temp_use])
@@ -218,7 +218,7 @@
    outstanding call for which no result has been produced.
 *)
 lemma RNext_enabled: "\<And>p. \<forall>l. basevars (mm!l, rtrner ch!p, rs!p) \<Longrightarrow>
-      \<turnstile> (rs!p = #NotAResult) & Calling ch p & (\<forall>l. MemInv mm l)
+      \<turnstile> (rs!p = #NotAResult) \<and> Calling ch p \<and> (\<forall>l. MemInv mm l)
          \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   apply (case_tac "arg (ch w p)")
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -63,7 +63,7 @@
 definition
   (* the environment action *)
   ENext         :: "PrIds \<Rightarrow> action"
-  where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
+  where "ENext p = ACT (\<exists>l. #l \<in> #MemLoc \<and> Call memCh p #(read l))"
 
 
 definition
@@ -74,7 +74,7 @@
 definition
   HNext         :: "histType \<Rightarrow> PrIds \<Rightarrow> action"
   where "HNext rmhist p = ACT (rmhist!p)$ =
-                     (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
+                     (if (MemReturn rmCh ires p \<or> RPCFail crCh rmCh rst p)
                       then #histB
                       else if (MClkReply memCh crCh cst p)
                            then #histA
@@ -83,7 +83,7 @@
 definition
   HistP         :: "histType \<Rightarrow> PrIds \<Rightarrow> temporal"
   where "HistP rmhist p = (TEMP Init HInit rmhist p
-                           & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
+                           \<and> \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
 
 definition
   Hist          :: "histType \<Rightarrow> temporal"
@@ -92,40 +92,40 @@
 definition
   (* the implementation *)
   IPImp          :: "PrIds \<Rightarrow> temporal"
-  where "IPImp p = (TEMP (  Init \<not>Calling memCh p & \<box>[ENext p]_(e p)
-                       & MClkIPSpec memCh crCh cst p
-                       & RPCIPSpec crCh rmCh rst p
-                       & RPSpec rmCh mm ires p
-                       & (\<forall>l. #l : #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
+  where "IPImp p = (TEMP (  Init \<not>Calling memCh p \<and> \<box>[ENext p]_(e p)
+                       \<and> MClkIPSpec memCh crCh cst p
+                       \<and> RPCIPSpec crCh rmCh rst p
+                       \<and> RPSpec rmCh mm ires p
+                       \<and> (\<forall>l. #l \<in> #MemLoc \<longrightarrow> MSpec rmCh mm ires l)))"
 
 definition
   ImpInit        :: "PrIds \<Rightarrow> stpred"
   where "ImpInit p = PRED (  \<not>Calling memCh p
-                          & MClkInit crCh cst p
-                          & RPCInit rmCh rst p
-                          & PInit ires p)"
+                          \<and> MClkInit crCh cst p
+                          \<and> RPCInit rmCh rst p
+                          \<and> PInit ires p)"
 
 definition
   ImpNext        :: "PrIds \<Rightarrow> action"
   where "ImpNext p = (ACT  [ENext p]_(e p)
-                       & [MClkNext memCh crCh cst p]_(c p)
-                       & [RPCNext crCh rmCh rst p]_(r p)
-                       & [RNext rmCh mm ires p]_(m p))"
+                       \<and> [MClkNext memCh crCh cst p]_(c p)
+                       \<and> [RPCNext crCh rmCh rst p]_(r p)
+                       \<and> [RNext rmCh mm ires p]_(m p))"
 
 definition
   ImpLive        :: "PrIds \<Rightarrow> temporal"
   where "ImpLive p = (TEMP  WF(MClkFwd memCh crCh cst p)_(c p)
-                        & SF(MClkReply memCh crCh cst p)_(c p)
-                        & WF(RPCNext crCh rmCh rst p)_(r p)
-                        & WF(RNext rmCh mm ires p)_(m p)
-                        & WF(MemReturn rmCh ires p)_(m p))"
+                        \<and> SF(MClkReply memCh crCh cst p)_(c p)
+                        \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+                        \<and> WF(RNext rmCh mm ires p)_(m p)
+                        \<and> WF(MemReturn rmCh ires p)_(m p))"
 
 definition
   Implementation :: "temporal"
-  where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) & \<box>[ENext p]_(e p))
-                               & MClkISpec memCh crCh cst
-                               & RPCISpec crCh rmCh rst
-                               & IRSpec rmCh mm ires))"
+  where "Implementation = (TEMP ( (\<forall>p. Init (\<not>Calling memCh p) \<and> \<box>[ENext p]_(e p))
+                               \<and> MClkISpec memCh crCh cst
+                               \<and> RPCISpec crCh rmCh rst
+                               \<and> IRSpec rmCh mm ires))"
 
 definition
   (* the predicate S describes the states of the implementation.
@@ -137,17 +137,17 @@
   S :: "histType \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> mClkState \<Rightarrow> rpcState \<Rightarrow> histState \<Rightarrow> histState \<Rightarrow> PrIds \<Rightarrow> stpred"
   where "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p = (PRED
                 Calling memCh p = #ecalling
-              & Calling crCh p  = #ccalling
-              & (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
-              & (\<not> #ccalling & cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
-              & Calling rmCh p  = #rcalling
-              & (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
-              & (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
-              & (\<not> #rcalling & rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
-              & cst!p = #cs
-              & rst!p = #rs
-              & (rmhist!p = #hs1 | rmhist!p = #hs2)
-              & MVNROKBA<ires!p>)"
+              \<and> Calling crCh p  = #ccalling
+              \<and> (#ccalling \<longrightarrow> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
+              \<and> (\<not> #ccalling \<and> cst!p = #clkB \<longrightarrow> MVOKBARF<res<crCh!p>>)
+              \<and> Calling rmCh p  = #rcalling
+              \<and> (#rcalling \<longrightarrow> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
+              \<and> (\<not> #rcalling \<longrightarrow> ires!p = #NotAResult)
+              \<and> (\<not> #rcalling \<and> rst!p = #rpcB \<longrightarrow> MVOKBA<res<rmCh!p>>)
+              \<and> cst!p = #cs
+              \<and> rst!p = #rs
+              \<and> (rmhist!p = #hs1 \<or> rmhist!p = #hs2)
+              \<and> MVNROKBA<ires!p>)"
 
 definition
   (* predicates S1 -- S6 define special instances of S *)
@@ -177,8 +177,8 @@
 definition
   (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
   ImpInv         :: "histType \<Rightarrow> PrIds \<Rightarrow> stpred"
-  where "ImpInv rmhist p = (PRED (S1 rmhist p | S2 rmhist p | S3 rmhist p
-                                | S4 rmhist p | S5 rmhist p | S6 rmhist p))"
+  where "ImpInv rmhist p = (PRED (S1 rmhist p \<or> S2 rmhist p \<or> S3 rmhist p
+                                \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p))"
 
 definition
   resbar        :: "histType \<Rightarrow> resType"        (* refinement mapping *)
@@ -241,9 +241,9 @@
 
 section "History variable"
 
-lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
+lemma HistoryLemma: "\<turnstile> Init(\<forall>p. ImpInit p) \<and> \<box>(\<forall>p. ImpNext p)
          \<longrightarrow> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
-                          & \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
+                          \<and> \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
   apply clarsimp
   apply (rule historyI)
       apply assumption+
@@ -299,21 +299,21 @@
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 *)
 
-lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p & \<not>S1 rmhist p"
+lemma S2_excl: "\<turnstile> S2 rmhist p \<longrightarrow> S2 rmhist p \<and> \<not>S1 rmhist p"
   by (auto simp: S_def S1_def S2_def)
 
-lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
+lemma S3_excl: "\<turnstile> S3 rmhist p \<longrightarrow> S3 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def)
 
-lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
+lemma S4_excl: "\<turnstile> S4 rmhist p \<longrightarrow> S4 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p \<and> \<not>S3 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def)
 
-lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
-                         & \<not>S3 rmhist p & \<not>S4 rmhist p"
+lemma S5_excl: "\<turnstile> S5 rmhist p \<longrightarrow> S5 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+                         \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
 
-lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
-                         & \<not>S3 rmhist p & \<not>S4 rmhist p & \<not>S5 rmhist p"
+lemma S6_excl: "\<turnstile> S6 rmhist p \<longrightarrow> S6 rmhist p \<and> \<not>S1 rmhist p \<and> \<not>S2 rmhist p
+                         \<and> \<not>S3 rmhist p \<and> \<not>S4 rmhist p \<and> \<not>S5 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 
 
@@ -331,24 +331,24 @@
 
 (* ------------------------------ State S1 ---------------------------------------- *)
 
-lemma S1Env: "\<turnstile> ENext p & $(S1 rmhist p) & unchanged (c p, r p, m p, rmhist!p)
+lemma S1Env: "\<turnstile> ENext p \<and> $(S1 rmhist p) \<and> unchanged (c p, r p, m p, rmhist!p)
          \<longrightarrow> (S2 rmhist p)$"
   by (force simp: ENext_def Call_def c_def r_def m_def
     caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
 
-lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S1ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (c p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] dest!: MClkidle [temp_use] simp: S_def S1_def)
 
-lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S1RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (r p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] dest!: RPCidle [temp_use] simp: S_def S1_def)
 
-lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S1MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S1 rmhist p) \<longrightarrow> unchanged (m p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] dest!: Memoryidle [temp_use] simp: S_def S1_def)
 
-lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
+lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p)
          \<longrightarrow> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
     @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
@@ -357,26 +357,26 @@
 
 (* ------------------------------ State S2 ---------------------------------------- *)
 
-lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S2EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (e p)"
   by (auto dest!: Envbusy [temp_use] simp: S_def S2_def)
 
-lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
+lemma S2Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S2 rmhist p) \<longrightarrow> MClkFwd memCh crCh cst p"
   by (auto simp: MClkNext_def MClkRetry_def MClkReply_def S_def S2_def)
 
-lemma S2Forward: "\<turnstile> $(S2 rmhist p) & MClkFwd memCh crCh cst p
-         & unchanged (e p, r p, m p, rmhist!p)
+lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p
+         \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> (S3 rmhist p)$"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
     @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
     @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
   by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
 
-lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S2MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S2_def dest!: Memoryidle [temp_use])
 
-lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
+lemma S2Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S2 rmhist p)
          \<longrightarrow> unchanged (rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -384,61 +384,61 @@
 
 (* ------------------------------ State S3 ---------------------------------------- *)
 
-lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S3EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (e p)"
   by (auto dest!: Envbusy [temp_use] simp: S_def S3_def)
 
-lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S3ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (c p)"
   by (auto dest!: MClkbusy [temp_use] simp: square_def S_def S3_def)
 
 lemma S3LegalRcvArg: "\<turnstile> S3 rmhist p \<longrightarrow> IsLegalRcvArg<arg<crCh!p>>"
   by (auto simp: IsLegalRcvArg_def MClkRelayArg_def S_def S3_def)
 
-lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S3 rmhist p)
-         \<longrightarrow> RPCFwd crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S3RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S3 rmhist p)
+         \<longrightarrow> RPCFwd crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
   apply clarsimp
   apply (frule S3LegalRcvArg [action_use])
   apply (auto simp: RPCNext_def RPCReject_def RPCReply_def S_def S3_def)
   done
 
-lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
-         & unchanged (e p, c p, m p)
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p \<and> HNext rmhist p \<and> $(S3 rmhist p)
+         \<and> unchanged (e p, c p, m p)
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
     @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
     @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
     @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
-         & unchanged (e p, c p, m p)
+lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p
+         \<and> unchanged (e p, c p, m p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
     @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
     @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
 
-lemma S3Hist: "\<turnstile> HNext rmhist p & $(S3 rmhist p) & unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
+lemma S3Hist: "\<turnstile> HNext rmhist p \<and> $(S3 rmhist p) \<and> unchanged (r p) \<longrightarrow> unchanged (rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
     Return_def r_def rtrner_def S_def S3_def Calling_def)
 
 (* ------------------------------ State S4 ---------------------------------------- *)
 
-lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S4EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (e p)"
   by (auto simp: S_def S4_def dest!: Envbusy [temp_use])
 
-lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S4ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (c p)"
   by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
 
-lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
+lemma S4RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S4 rmhist p) \<longrightarrow> unchanged (r p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] dest!: RPCbusy [temp_use] simp: S_def S4_def)
 
-lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
-         & HNext rmhist p & $(MemInv mm l)
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+         \<and> HNext rmhist p \<and> $(MemInv mm l)
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
     @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
     @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
@@ -446,68 +446,68 @@
     @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
     @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
 
-lemma S4Read: "\<turnstile> Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
-         & HNext rmhist p & (\<forall>l. $MemInv mm l)
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Read: "\<turnstile> Read rmCh mm ires p \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+         \<and> HNext rmhist p \<and> (\<forall>l. $MemInv mm l)
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (auto simp: Read_def dest!: S4ReadInner [temp_use])
 
-lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) \<and> HNext rmhist p
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
     @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
     @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
     @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S4Write: "\<turnstile> Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
-         & (HNext rmhist p)
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (rmhist!p)"
+lemma S4Write: "\<turnstile> Write rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
+         \<and> (HNext rmhist p)
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (auto simp: Write_def dest!: S4WriteInner [temp_use])
 
-lemma WriteS4: "\<turnstile> $ImpInv rmhist p & Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
+lemma WriteS4: "\<turnstile> $ImpInv rmhist p \<and> Write rmCh mm ires p l \<longrightarrow> $S4 rmhist p"
   by (auto simp: Write_def WriteInner_def ImpInv_def
     WrRequest_def S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 
-lemma S4Return: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & unchanged (e p, c p, r p)
-         & HNext rmhist p
+lemma S4Return: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> unchanged (e p, c p, r p)
+         \<and> HNext rmhist p
          \<longrightarrow> (S5 rmhist p)$"
   by (auto simp: HNext_def MemReturn_def Return_def e_def c_def r_def
     rtrner_def caller_def MVNROKBA_def MVOKBA_def S_def S4_def S5_def Calling_def)
 
-lemma S4Hist: "\<turnstile> HNext rmhist p & $S4 rmhist p & (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S4Hist: "\<turnstile> HNext rmhist p \<and> $S4 rmhist p \<and> (m p)$ = $(m p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   by (auto simp: HNext_def MemReturn_def RPCFail_def MClkReply_def
     Return_def m_def rtrner_def S_def S4_def Calling_def)
 
 (* ------------------------------ State S5 ---------------------------------------- *)
 
-lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S5EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (e p)"
   by (auto simp: S_def S5_def dest!: Envbusy [temp_use])
 
-lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) & $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
+lemma S5ClerkUnch: "\<turnstile> [MClkNext memCh crCh cst p]_(c p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (c p)"
   by (auto simp: S_def S5_def dest!: MClkbusy [temp_use])
 
-lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p & $(S5 rmhist p)
-         \<longrightarrow> RPCReply crCh rmCh rst p | RPCFail crCh rmCh rst p"
+lemma S5RPC: "\<turnstile> RPCNext crCh rmCh rst p \<and> $(S5 rmhist p)
+         \<longrightarrow> RPCReply crCh rmCh rst p \<or> RPCFail crCh rmCh rst p"
   by (auto simp: RPCNext_def RPCReject_def RPCFwd_def S_def S5_def)
 
-lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
        \<longrightarrow> (S6 rmhist p)$"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
     @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
     @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
+lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
          \<longrightarrow> (S6 rmhist p)$"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
     @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
 
-lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
+lemma S5Hist: "\<turnstile> [HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> $(S5 rmhist p)
          \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: HNext_def MemReturn_def RPCFail_def
@@ -515,36 +515,36 @@
 
 (* ------------------------------ State S6 ---------------------------------------- *)
 
-lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) & $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
+lemma S6EnvUnch: "\<turnstile> [ENext p]_(e p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (e p)"
   by (auto simp: S_def S6_def dest!: Envbusy [temp_use])
 
-lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p & $(S6 rmhist p)
-         \<longrightarrow> MClkRetry memCh crCh cst p | MClkReply memCh crCh cst p"
+lemma S6Clerk: "\<turnstile> MClkNext memCh crCh cst p \<and> $(S6 rmhist p)
+         \<longrightarrow> MClkRetry memCh crCh cst p \<or> MClkReply memCh crCh cst p"
   by (auto simp: MClkNext_def MClkFwd_def S_def S6_def)
 
-lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
-         & unchanged (e p,r p,m p)
-         \<longrightarrow> (S3 rmhist p)$ & unchanged (rmhist!p)"
+lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+         \<and> unchanged (e p,r p,m p)
+         \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
-         & unchanged (e p,r p,m p)
+lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
+         \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S1 rmhist p)$"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
     @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
 
-lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p \<longrightarrow> unchanged (r p)"
+lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)"
   by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
 
-lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) & $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
+lemma S6MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S6 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S6_def dest!: Memoryidle [temp_use])
 
-lemma S6Hist: "\<turnstile> HNext rmhist p & $S6 rmhist p & (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
+lemma S6Hist: "\<turnstile> HNext rmhist p \<and> $S6 rmhist p \<and> (c p)$ = $(c p) \<longrightarrow> (rmhist!p)$ = $(rmhist!p)"
   by (auto simp: HNext_def MClkReply_def Return_def c_def rtrner_def S_def S6_def Calling_def)
 
 
@@ -554,7 +554,7 @@
 (* ========== Step 1.1 ================================================= *)
 (* The implementation's initial condition implies the state predicate S1 *)
 
-lemma Step1_1: "\<turnstile> ImpInit p & HInit rmhist p \<longrightarrow> S1 rmhist p"
+lemma Step1_1: "\<turnstile> ImpInit p \<and> HInit rmhist p \<longrightarrow> S1 rmhist p"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: MVNROKBA_def
     MClkInit_def RPCInit_def PInit_def HInit_def ImpInit_def S_def S1_def)
@@ -562,9 +562,9 @@
 (* ========== Step 1.2 ================================================== *)
 (* Figure 16 is a predicate-action diagram for the implementation. *)
 
-lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & \<not>unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
-         \<longrightarrow> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
+lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+         \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p)  \<and> $S1 rmhist p
+         \<longrightarrow> (S2 rmhist p)$ \<and> ENext p \<and> unchanged (c p, r p, m p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
       (map (temp_elim @{context})
         [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
@@ -572,10 +572,10 @@
    apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   done
 
-lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
-         \<longrightarrow> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
-             & unchanged (e p, r p, m p, rmhist!p)"
+lemma Step1_2_2: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+         \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S2 rmhist p
+         \<longrightarrow> (S3 rmhist p)$ \<and> MClkFwd memCh crCh cst p
+             \<and> unchanged (e p, r p, m p, rmhist!p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context})
       [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
@@ -583,10 +583,10 @@
    apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   done
 
-lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
-         \<longrightarrow> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
-             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_3: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+         \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S3 rmhist p
+         \<longrightarrow> ((S4 rmhist p)$ \<and> RPCFwd crCh rmCh rst p \<and> unchanged (e p, c p, m p, rmhist!p))
+             \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
   apply (tactic {* action_simp_tac @{context} []
@@ -595,12 +595,12 @@
    apply (auto dest!: S3Hist [temp_use])
   done
 
-lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & \<not>unchanged (e p, c p, r p, m p, rmhist!p)
-              & $S4 rmhist p & (\<forall>l. $(MemInv mm l))
-         \<longrightarrow> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
-             | ((S4 rmhist p)$ & (\<exists>l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
-             | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
+lemma Step1_2_4: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+              \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p)
+              \<and> $S4 rmhist p \<and> (\<forall>l. $(MemInv mm l))
+         \<longrightarrow> ((S4 rmhist p)$ \<and> Read rmCh mm ires p \<and> unchanged (e p, c p, r p, rmhist!p))
+             \<or> ((S4 rmhist p)$ \<and> (\<exists>l. Write rmCh mm ires p l) \<and> unchanged (e p, c p, r p, rmhist!p))
+             \<or> ((S5 rmhist p)$ \<and> MemReturn rmCh ires p \<and> unchanged (e p, c p, r p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
@@ -609,10 +609,10 @@
   apply (auto dest!: S4Hist [temp_use])
   done
 
-lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
-         \<longrightarrow> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
-             | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
+lemma Step1_2_5: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+              \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S5 rmhist p
+         \<longrightarrow> ((S6 rmhist p)$ \<and> RPCReply crCh rmCh rst p \<and> unchanged (e p, c p, m p))
+             \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
   apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
@@ -620,10 +620,10 @@
    apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   done
 
-lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
-         \<longrightarrow> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
-             | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
+lemma Step1_2_6: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
+              \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S6 rmhist p
+         \<longrightarrow> ((S1 rmhist p)$ \<and> MClkReply memCh crCh cst p \<and> unchanged (e p, r p, m p))
+             \<or> ((S3 rmhist p)$ \<and> MClkRetry memCh crCh cst p \<and> unchanged (e p,r p,m p,rmhist!p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
   apply (tactic {* action_simp_tac @{context} []
@@ -648,20 +648,20 @@
 
 section "Step simulation (Step 1.4)"
 
-lemma Step1_4_1: "\<turnstile> ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
+lemma Step1_4_1: "\<turnstile> ENext p \<and> $S1 rmhist p \<and> (S2 rmhist p)$ \<and> unchanged (c p, r p, m p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   using [[fast_solver]]
   by (auto elim!: squareE [temp_use] simp: c_def r_def m_def resbar_def)
 
-lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
-         & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p \<and> $S2 rmhist p \<and> (S3 rmhist p)$
+         \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   by (tactic {* action_simp_tac
     (@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
     @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
 
-lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
-         & unchanged (e p, c p, m p, rmhist!p)
+lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p \<and> $S3 rmhist p \<and> (S4 rmhist p)$
+         \<and> unchanged (e p, c p, m p, rmhist!p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (drule S3_excl [temp_use] S4_excl [temp_use])+
@@ -669,8 +669,8 @@
     @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
   done
 
-lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
-         & unchanged (e p, c p, m p)
+lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S3 rmhist p \<and> (S6 rmhist p)$
+         \<and> unchanged (e p, c p, m p)
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])
@@ -679,8 +679,8 @@
    apply (auto simp: Return_def)
   done
 
-lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & ReadInner rmCh mm ires p l
-         & unchanged (e p, c p, r p, rmhist!p) & $MemInv mm l
+lemma Step1_4_4a1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> ReadInner rmCh mm ires p l
+         \<and> unchanged (e p, c p, r p, rmhist!p) \<and> $MemInv mm l
          \<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
@@ -693,13 +693,13 @@
                 [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
   done
 
-lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
-         & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
+lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+         \<and> unchanged (e p, c p, r p, rmhist!p) \<and> (\<forall>l. $(MemInv mm l))
          \<longrightarrow> Read memCh mm (resbar rmhist) p"
   by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
 
-lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p & (S4 rmhist p)$ & WriteInner rmCh mm ires p l v
-         & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b1: "\<turnstile> $S4 rmhist p \<and> (S4 rmhist p)$ \<and> WriteInner rmCh mm ires p l v
+         \<and> unchanged (e p, c p, r p, rmhist!p)
          \<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
@@ -712,13 +712,13 @@
       @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
   done
 
-lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
-         & unchanged (e p, c p, r p, rmhist!p)
+lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l \<and> $S4 rmhist p \<and> (S4 rmhist p)$
+         \<and> unchanged (e p, c p, r p, rmhist!p)
          \<longrightarrow> Write memCh mm (resbar rmhist) p l"
   by (force simp: Write_def elim!: Step1_4_4b1 [temp_use])
 
-lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
-         & unchanged (e p, c p, r p)
+lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> (S5 rmhist p)$
+         \<and> unchanged (e p, c p, r p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
@@ -727,8 +727,8 @@
   apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
   done
 
-lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
-         & unchanged (e p, c p, m p)
+lemma Step1_4_5a: "\<turnstile> RPCReply crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+         \<and> unchanged (e p, c p, m p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (drule S5_excl [temp_use] S6_excl [temp_use])+
@@ -736,8 +736,8 @@
    apply (auto simp: RPCReply_def Return_def S5_def S_def dest!: MVOKBAnotRF [temp_use])
   done
 
-lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
-         & unchanged (e p, c p, m p)
+lemma Step1_4_5b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S5 rmhist p \<and> (S6 rmhist p)$
+         \<and> unchanged (e p, c p, m p)
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])
@@ -745,8 +745,8 @@
    apply (auto simp: S5_def S_def)
   done
 
-lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p & $S6 rmhist p & (S1 rmhist p)$
-         & unchanged (e p, r p, m p)
+lemma Step1_4_6a: "\<turnstile> MClkReply memCh crCh cst p \<and> $S6 rmhist p \<and> (S1 rmhist p)$
+         \<and> unchanged (e p, r p, m p)
          \<longrightarrow> MemReturn memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])+
@@ -758,8 +758,8 @@
       [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
   done
 
-lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
-         & unchanged (e p, r p, m p, rmhist!p)
+lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p \<and> $S6 rmhist p \<and> (S3 rmhist p)$
+         \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S3_excl [temp_use])+
@@ -825,7 +825,7 @@
 (* turn into (unsafe, looping!) introduction rule *)
 lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
 
-lemma S1safe: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S1safe: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -833,7 +833,7 @@
   apply (auto dest!: Step1_2_1 [temp_use] Step1_4_1 [temp_use])
   done
 
-lemma S2safe: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2safe: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -841,7 +841,7 @@
   apply (auto dest!: Step1_2_2 [temp_use] Step1_4_2 [temp_use])
   done
 
-lemma S3safe: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3safe: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -849,8 +849,8 @@
   apply (auto simp: square_def UNext_def dest!: Step1_4_3a [temp_use] Step1_4_3b [temp_use])
   done
 
-lemma S4safe: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (\<forall>l. $(MemInv mm l))
+lemma S4safe: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<and> (\<forall>l. $(MemInv mm l))
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -859,7 +859,7 @@
        dest!: Step1_4_4a [temp_use] Step1_4_4b [temp_use] Step1_4_4c [temp_use])
   done
 
-lemma S5safe: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5safe: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -867,7 +867,7 @@
   apply (auto simp: square_def UNext_def dest!: Step1_4_5a [temp_use] Step1_4_5b [temp_use])
   done
 
-lemma S6safe: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S6safe: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -889,8 +889,8 @@
 
 (* ------------------------------ State S1 ------------------------------ *)
 
-lemma S1_successors: "\<turnstile> $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         \<longrightarrow> (S1 rmhist p)$ | (S2 rmhist p)$"
+lemma S1_successors: "\<turnstile> $S1 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<longrightarrow> (S1 rmhist p)$ \<or> (S2 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_1 [temp_use])
   done
@@ -923,18 +923,18 @@
 
 (* ------------------------------ State S2 ------------------------------ *)
 
-lemma S2_successors: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         \<longrightarrow> (S2 rmhist p)$ | (S3 rmhist p)$"
+lemma S2_successors: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<longrightarrow> (S2 rmhist p)$ \<or> (S3 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_2 [temp_use])
   done
 
-lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & <MClkFwd memCh crCh cst p>_(c p)
+lemma S2MClkFwd_successors: "\<turnstile> ($S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> <MClkFwd memCh crCh cst p>_(c p)
          \<longrightarrow> (S3 rmhist p)$"
   by (auto simp: angle_def dest!: Step1_2_2 [temp_use])
 
-lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S2MClkFwd_enabled: "\<turnstile> $S2 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> $Enabled (<MClkFwd memCh crCh cst p>_(c p))"
   apply (auto simp: c_def intro!: MClkFwd_ch_enabled [temp_use] MClkFwd_enabled [temp_use])
      apply (cut_tac MI_base)
@@ -942,26 +942,26 @@
     apply (simp_all add: S_def S2_def)
   done
 
-lemma S2_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & WF(MClkFwd memCh crCh cst p)_(c p)
+lemma S2_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> WF(MClkFwd memCh crCh cst p)_(c p)
          \<longrightarrow> (S2 rmhist p \<leadsto> S3 rmhist p)"
   by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
 
 (* ------------------------------ State S3 ------------------------------ *)
 
-lemma S3_successors: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         \<longrightarrow> (S3 rmhist p)$ | (S4 rmhist p | S6 rmhist p)$"
+lemma S3_successors: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<longrightarrow> (S3 rmhist p)$ \<or> (S4 rmhist p \<or> S6 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_3 [temp_use])
   done
 
-lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & <RPCNext crCh rmCh rst p>_(r p)
-         \<longrightarrow> (S4 rmhist p | S6 rmhist p)$"
+lemma S3RPC_successors: "\<turnstile> ($S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> <RPCNext crCh rmCh rst p>_(r p)
+         \<longrightarrow> (S4 rmhist p \<or> S6 rmhist p)$"
   apply (auto simp: angle_def dest!: Step1_2_3 [temp_use])
   done
 
-lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S3RPC_enabled: "\<turnstile> $S3 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
   apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
     apply (cut_tac MI_base)
@@ -969,39 +969,39 @@
    apply (simp_all add: S_def S3_def)
   done
 
-lemma S3_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & WF(RPCNext crCh rmCh rst p)_(r p)
-         \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
+lemma S3_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> WF(RPCNext crCh rmCh rst p)_(r p)
+         \<longrightarrow> (S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p)"
   by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
 
 (* ------------- State S4 -------------------------------------------------- *)
 
-lemma S4_successors: "\<turnstile> $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-        & (\<forall>l. $MemInv mm l)
-        \<longrightarrow> (S4 rmhist p)$ | (S5 rmhist p)$"
+lemma S4_successors: "\<turnstile> $S4 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+        \<and> (\<forall>l. $MemInv mm l)
+        \<longrightarrow> (S4 rmhist p)$ \<or> (S5 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
 
-lemma S4a_successors: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
-         \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult)$
-             | ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4a_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+         \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult)$
+             \<or> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
-lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l))
-         & <RNext rmCh mm ires p>_(m p)
-         \<longrightarrow> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
+lemma S4aRNext_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p = #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+         \<and> <RNext rmCh mm ires p>_(m p)
+         \<longrightarrow> ((S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)$"
   by (auto simp: angle_def
     dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
 
-lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
+lemma S4aRNext_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p = #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
          \<longrightarrow> $Enabled (<RNext rmCh mm ires p>_(m p))"
   apply (auto simp: m_def intro!: RNext_enabled [temp_use])
    apply (cut_tac MI_base)
@@ -1009,30 +1009,30 @@
   apply (simp add: S_def S4_def)
   done
 
-lemma S4a_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (\<forall>l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
-         \<longrightarrow> (S4 rmhist p & ires!p = #NotAResult
-              \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
+lemma S4a_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<and> (\<forall>l. $MemInv mm l)) \<and> WF(RNext rmCh mm ires p)_(m p)
+         \<longrightarrow> (S4 rmhist p \<and> ires!p = #NotAResult
+              \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p)"
   by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
 
 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
 
-lemma S4b_successors: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
-         \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (S5 rmhist p)$"
+lemma S4b_successors: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l)
+         \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult)$ \<or> (S5 rmhist p)$"
   apply (split_idle simp: m_def)
   apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
   done
 
-lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
+lemma S4bReturn_successors: "\<turnstile> ($(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<and> (\<forall>l. $MemInv mm l)) \<and> <MemReturn rmCh ires p>_(m p)
          \<longrightarrow> (S5 rmhist p)$"
   by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
 
-lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p & ires!p \<noteq> #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (\<forall>l. $MemInv mm l)
+lemma S4bReturn_enabled: "\<turnstile> $(S4 rmhist p \<and> ires!p \<noteq> #NotAResult)
+         \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<and> (\<forall>l. $MemInv mm l)
          \<longrightarrow> $Enabled (<MemReturn rmCh ires p>_(m p))"
   apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
    apply (cut_tac MI_base)
@@ -1040,25 +1040,25 @@
   apply (simp add: S_def S4_def)
   done
 
-lemma S4b_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l))
-         & WF(MemReturn rmCh ires p)_(m p)
-         \<longrightarrow> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
+lemma S4b_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> (\<forall>l. $MemInv mm l))
+         \<and> WF(MemReturn rmCh ires p)_(m p)
+         \<longrightarrow> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
   by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
 
 (* ------------------------------ State S5 ------------------------------ *)
 
-lemma S5_successors: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         \<longrightarrow> (S5 rmhist p)$ | (S6 rmhist p)$"
+lemma S5_successors: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<longrightarrow> (S5 rmhist p)$ \<or> (S6 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_5 [temp_use])
   done
 
-lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & <RPCNext crCh rmCh rst p>_(r p)
+lemma S5RPC_successors: "\<turnstile> ($S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> <RPCNext crCh rmCh rst p>_(r p)
          \<longrightarrow> (S6 rmhist p)$"
   by (auto simp: angle_def dest!: Step1_2_5 [temp_use])
 
-lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+lemma S5RPC_enabled: "\<turnstile> $S5 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
          \<longrightarrow> $Enabled (<RPCNext crCh rmCh rst p>_(r p))"
   apply (auto simp: r_def intro!: RPCFail_Next_enabled [temp_use] RPCFail_enabled [temp_use])
     apply (cut_tac MI_base)
@@ -1066,27 +1066,27 @@
    apply (simp_all add: S_def S5_def)
   done
 
-lemma S5_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & WF(RPCNext crCh rmCh rst p)_(r p)
+lemma S5_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> WF(RPCNext crCh rmCh rst p)_(r p)
          \<longrightarrow> (S5 rmhist p \<leadsto> S6 rmhist p)"
   by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
 
 (* ------------------------------ State S6 ------------------------------ *)
 
-lemma S6_successors: "\<turnstile> $S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         \<longrightarrow> (S1 rmhist p)$ | (S3 rmhist p)$ | (S6 rmhist p)$"
+lemma S6_successors: "\<turnstile> $S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p)
+         \<longrightarrow> (S1 rmhist p)$ \<or> (S3 rmhist p)$ \<or> (S6 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_6 [temp_use])
   done
 
 lemma S6MClkReply_successors:
-  "\<turnstile> ($S6 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
-         & <MClkReply memCh crCh cst p>_(c p)
+  "\<turnstile> ($S6 rmhist p \<and> ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+         \<and> <MClkReply memCh crCh cst p>_(c p)
          \<longrightarrow> (S1 rmhist p)$"
   by (auto simp: angle_def dest!: Step1_2_6 [temp_use] MClkReplyNotRetry [temp_use])
 
 lemma MClkReplyS6:
-  "\<turnstile> $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
+  "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
     @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
     @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
@@ -1099,8 +1099,8 @@
       addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
   done
 
-lemma S6_live: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
-         & SF(MClkReply memCh crCh cst p)_(c p) & \<box>\<diamond>(S6 rmhist p)
+lemma S6_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> $(ImpInv rmhist p))
+         \<and> SF(MClkReply memCh crCh cst p)_(c p) \<and> \<box>\<diamond>(S6 rmhist p)
          \<longrightarrow> \<box>\<diamond>(S1 rmhist p)"
   apply clarsimp
   apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
@@ -1116,25 +1116,25 @@
 (* --------------- aggregate leadsto properties----------------------------- *)
 
 lemma S5S6LeadstoS6: "sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p
-      \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
+      \<Longrightarrow> sigma \<Turnstile> (S5 rmhist p \<or> S6 rmhist p) \<leadsto> S6 rmhist p"
   by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
 
-lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4bS5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
          sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
-      \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
+      \<Longrightarrow> sigma \<Turnstile> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p
                     \<leadsto> S6 rmhist p"
   by (auto intro!: LatticeDisjunctionIntro [temp_use]
     S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
 
-lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
-                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+                  \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
          sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
-      \<Longrightarrow> sigma \<Turnstile> S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
-  apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p & ires!p = #NotAResult) |
-    (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p")
-   apply (erule_tac G = "PRED ((S4 rmhist p & ires!p = #NotAResult) |
-     (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p)" in
+      \<Longrightarrow> sigma \<Turnstile> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
+  apply (subgoal_tac "sigma \<Turnstile> (S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+    (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p")
+   apply (erule_tac G = "PRED ((S4 rmhist p \<and> ires!p = #NotAResult) \<or>
+     (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p \<or> S6 rmhist p)" in
      LatticeTransitivity [temp_use])
    apply (force simp: Init_defs intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
   apply (rule LatticeDisjunctionIntro [temp_use])
@@ -1144,12 +1144,12 @@
   apply (auto intro!: S4bS5S6LeadstoS6 [temp_use])
   done
 
-lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
-                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+lemma S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+                  \<leadsto> (S4 rmhist p \<and> ires!p \<noteq> #NotAResult) \<or> S5 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
          sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
-      \<Longrightarrow> sigma \<Turnstile> S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
+      \<Longrightarrow> sigma \<Turnstile> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p \<leadsto> S6 rmhist p"
   apply (rule LatticeDisjunctionIntro [temp_use])
    apply (erule LatticeTriangle2 [temp_use])
    apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1158,12 +1158,12 @@
   done
 
 lemma S2S3S4S5S6LeadstoS6: "\<lbrakk> sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
-         sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
-                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+                  \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
          sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
-      \<Longrightarrow> sigma \<Turnstile> S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
+      \<Longrightarrow> sigma \<Turnstile> S2 rmhist p \<or> S3 rmhist p \<or> S4 rmhist p \<or> S5 rmhist p \<or> S6 rmhist p
                    \<leadsto> S6 rmhist p"
   apply (rule LatticeDisjunctionIntro [temp_use])
    apply (rule LatticeTransitivity [temp_use])
@@ -1175,10 +1175,10 @@
 
 lemma NotS1LeadstoS6: "\<lbrakk> sigma \<Turnstile> \<box>ImpInv rmhist p;
          sigma \<Turnstile> S2 rmhist p \<leadsto> S3 rmhist p;
-         sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p = #NotAResult
-                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
-         sigma \<Turnstile> S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma \<Turnstile> S3 rmhist p \<leadsto> S4 rmhist p \<or> S6 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p = #NotAResult
+                  \<leadsto> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<or> S5 rmhist p;
+         sigma \<Turnstile> S4 rmhist p \<and> ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
          sigma \<Turnstile> S5 rmhist p \<leadsto> S6 rmhist p \<rbrakk>
       \<Longrightarrow> sigma \<Turnstile> \<not>S1 rmhist p \<leadsto> S6 rmhist p"
   apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1207,8 +1207,8 @@
 lemma Step1_5_1a: "\<turnstile> IPImp p \<longrightarrow> (\<forall>l. \<box>$MemInv mm l)"
   by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
 
-lemma Step1_5_1b: "\<turnstile> Init(ImpInit p & HInit rmhist p) & \<box>(ImpNext p)
-         & \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) & \<box>(\<forall>l. $MemInv mm l)
+lemma Step1_5_1b: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<and> \<box>(ImpNext p)
+         \<and> \<box>[HNext rmhist p]_(c p, r p, m p, rmhist!p) \<and> \<box>(\<forall>l. $MemInv mm l)
          \<longrightarrow> \<box>ImpInv rmhist p"
   apply invariant
    apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
@@ -1218,26 +1218,26 @@
   done
 
 (*** Initialization ***)
-lemma Step1_5_2a: "\<turnstile> Init(ImpInit p & HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
+lemma Step1_5_2a: "\<turnstile> Init(ImpInit p \<and> HInit rmhist p) \<longrightarrow> Init(PInit (resbar rmhist) p)"
   by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
 
 (*** step simulation ***)
-lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
-         & $ImpInv rmhist p & (\<forall>l. $MemInv mm l))
+lemma Step1_5_2b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+         \<and> $ImpInv rmhist p \<and> (\<forall>l. $MemInv mm l))
          \<longrightarrow> \<box>[UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   by (auto simp: ImpInv_def elim!: STL4E [temp_use]
     dest!: S1safe [temp_use] S2safe [temp_use] S3safe [temp_use] S4safe [temp_use]
     S5safe [temp_use] S6safe [temp_use])
 
 (*** Liveness ***)
-lemma GoodImpl: "\<turnstile> IPImp p & HistP rmhist p
-         \<longrightarrow>   Init(ImpInit p & HInit rmhist p)
-             & \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-             & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p)
-             & ImpLive p"
+lemma GoodImpl: "\<turnstile> IPImp p \<and> HistP rmhist p
+         \<longrightarrow>   Init(ImpInit p \<and> HInit rmhist p)
+             \<and> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+             \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p)
+             \<and> ImpLive p"
   apply clarsimp
-    apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p & HInit rmhist p) & \<box> (ImpNext p) &
-      \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) & \<box> (\<forall>l. $MemInv mm l)")
+    apply (subgoal_tac "sigma \<Turnstile> Init (ImpInit p \<and> HInit rmhist p) \<and> \<box> (ImpNext p) \<and>
+      \<box>[HNext rmhist p]_ (c p, r p, m p, rmhist!p) \<and> \<box> (\<forall>l. $MemInv mm l)")
    apply (auto simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
        dest!: Step1_5_1b [temp_use])
       apply (force simp: IPImp_def MClkIPSpec_def RPCIPSpec_def RPSpec_def
@@ -1251,9 +1251,9 @@
   done
 
 (* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & \<box>(\<forall>l. $MemInv mm l)
-         & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3a: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+         \<and> \<box>(\<forall>l. $MemInv mm l)
+         \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
          \<longrightarrow> \<box>\<diamond>S1 rmhist p"
   apply (clarsimp simp: ImpLive_def)
   apply (rule S1Infinite)
@@ -1264,18 +1264,18 @@
   done
 
 (* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3b: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+         \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
          \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   by (auto intro!: RNext_fair [temp_use] Step1_5_3a [temp_use])
 
-lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & \<box>(\<forall>l. $MemInv mm l) & \<box>($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3c: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+         \<and> \<box>(\<forall>l. $MemInv mm l) \<and> \<box>($ImpInv rmhist p) \<and> ImpLive p
          \<longrightarrow> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
 
 (* QED step of step 1 *)
-lemma Step1: "\<turnstile> IPImp p & HistP rmhist p --> UPSpec memCh mm (resbar rmhist) p"
+lemma Step1: "\<turnstile> IPImp p \<and> HistP rmhist p \<longrightarrow> UPSpec memCh mm (resbar rmhist) p"
   by (auto simp: UPSpec_def split_box_conj [temp_use]
     dest!: GoodImpl [temp_use] intro!: Step1_5_2a [temp_use] Step1_5_2b [temp_use]
     Step1_5_3b [temp_use] Step1_5_3c [temp_use])
@@ -1283,10 +1283,10 @@
 (* ------------------------------ Step 2 ------------------------------ *)
 section "Step 2"
 
-lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l & ImpNext p
-         & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
-         & $ImpInv rmhist p
-         \<longrightarrow> (S4 rmhist p)$ & unchanged (e p, c p, r p, rmhist!p)"
+lemma Step2_2a: "\<turnstile> Write rmCh mm ires p l \<and> ImpNext p
+         \<and> [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+         \<and> $ImpInv rmhist p
+         \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (e p, c p, r p, rmhist!p)"
   apply clarsimp
   apply (drule WriteS4 [action_use])
    apply assumption
@@ -1297,9 +1297,9 @@
   done
 
 lemma Step2_2: "\<turnstile>   (\<forall>p. ImpNext p)
-         & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & (\<forall>p. $ImpInv rmhist p)
-         & [\<exists>q. Write rmCh mm ires q l]_(mm!l)
+         \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+         \<and> (\<forall>p. $ImpInv rmhist p)
+         \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l)
          \<longrightarrow> [\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   apply (auto intro!: squareCI elim!: squareE)
   apply (assumption | rule exI Step1_4_4b [action_use])+
@@ -1308,13 +1308,13 @@
   done
 
 lemma Step2_lemma: "\<turnstile> \<box>(  (\<forall>p. ImpNext p)
-            & (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-            & (\<forall>p. $ImpInv rmhist p)
-            & [\<exists>q. Write rmCh mm ires q l]_(mm!l))
+            \<and> (\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
+            \<and> (\<forall>p. $ImpInv rmhist p)
+            \<and> [\<exists>q. Write rmCh mm ires q l]_(mm!l))
          \<longrightarrow> \<box>[\<exists>q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
   by (force elim!: STL4E [temp_use] dest!: Step2_2 [temp_use])
 
-lemma Step2: "\<turnstile> #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
+lemma Step2: "\<turnstile> #l \<in> #MemLoc \<and> (\<forall>p. IPImp p \<and> HistP rmhist p)
          \<longrightarrow> MSpec memCh mm (resbar rmhist) l"
   apply (auto simp: MSpec_def)
    apply (force simp: IPImp_def MSpec_def)
@@ -1334,7 +1334,7 @@
 (* Implementation of internal specification by combination of implementation
    and history variable with explicit refinement mapping
 *)
-lemma Impl_IUSpec: "\<turnstile> Implementation & Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
+lemma Impl_IUSpec: "\<turnstile> Implementation \<and> Hist rmhist \<longrightarrow> IUSpec memCh mm (resbar rmhist)"
   by (auto simp: IUSpec_def Implementation_def IPImp_def MClkISpec_def
     RPCISpec_def IRSpec_def Hist_def intro!: Step1 [temp_use] Step2 [temp_use])
 
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -63,14 +63,14 @@
 
   Calling_def:   "Calling ch p  == PRED cbit< ch!p > \<noteq> rbit< ch!p >"
   Call_def:      "(ACT Call ch p v)   == ACT  \<not> $Calling ch p
-                                     & (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
-                                     & (arg<ch!p>$ = $v)"
+                                     \<and> (cbit<ch!p>$ \<noteq> $rbit<ch!p>)
+                                     \<and> (arg<ch!p>$ = $v)"
   Return_def:    "(ACT Return ch p v) == ACT  $Calling ch p
-                                     & (rbit<ch!p>$ = $cbit<ch!p>)
-                                     & (res<ch!p>$ = $v)"
+                                     \<and> (rbit<ch!p>$ = $cbit<ch!p>)
+                                     \<and> (res<ch!p>$ = $v)"
   PLegalCaller_def:      "PLegalCaller ch p == TEMP
                              Init(\<not> Calling ch p)
-                             & \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
+                             \<and> \<box>[\<exists>a. Call ch p a ]_((caller ch)!p)"
   LegalCaller_def:       "LegalCaller ch == TEMP (\<forall>p. PLegalCaller ch p)"
   PLegalReturner_def:    "PLegalReturner ch p == TEMP
                                 \<box>[\<exists>v. Return ch p v ]_((rtrner ch)!p)"
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -28,45 +28,45 @@
   RPCISpec   :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
 
 defs
-  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
+  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
 
   RPCFwd_def:        "RPCFwd send rcv rst p == ACT
                          $(Calling send p)
-                         & $(rst!p) = # rpcA
-                         & IsLegalRcvArg<arg<$(send!p)>>
-                         & Call rcv p RPCRelayArg<arg<send!p>>
-                         & (rst!p)$ = # rpcB
-                         & unchanged (rtrner send!p)"
+                         \<and> $(rst!p) = # rpcA
+                         \<and> IsLegalRcvArg<arg<$(send!p)>>
+                         \<and> Call rcv p RPCRelayArg<arg<send!p>>
+                         \<and> (rst!p)$ = # rpcB
+                         \<and> unchanged (rtrner send!p)"
 
   RPCReject_def:     "RPCReject send rcv rst p == ACT
                            $(rst!p) = # rpcA
-                         & \<not>IsLegalRcvArg<arg<$(send!p)>>
-                         & Return send p #BadCall
-                         & unchanged ((rst!p), (caller rcv!p))"
+                         \<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
+                         \<and> Return send p #BadCall
+                         \<and> unchanged ((rst!p), (caller rcv!p))"
 
   RPCFail_def:       "RPCFail send rcv rst p == ACT
                            \<not>$(Calling rcv p)
-                         & Return send p #RPCFailure
-                         & (rst!p)$ = #rpcA
-                         & unchanged (caller rcv!p)"
+                         \<and> Return send p #RPCFailure
+                         \<and> (rst!p)$ = #rpcA
+                         \<and> unchanged (caller rcv!p)"
 
   RPCReply_def:      "RPCReply send rcv rst p == ACT
                            \<not>$(Calling rcv p)
-                         & $(rst!p) = #rpcB
-                         & Return send p res<rcv!p>
-                         & (rst!p)$ = #rpcA
-                         & unchanged (caller rcv!p)"
+                         \<and> $(rst!p) = #rpcB
+                         \<and> Return send p res<rcv!p>
+                         \<and> (rst!p)$ = #rpcA
+                         \<and> unchanged (caller rcv!p)"
 
   RPCNext_def:       "RPCNext send rcv rst p == ACT
                         (  RPCFwd send rcv rst p
-                         | RPCReject send rcv rst p
-                         | RPCFail send rcv rst p
-                         | RPCReply send rcv rst p)"
+                         \<or> RPCReject send rcv rst p
+                         \<or> RPCFail send rcv rst p
+                         \<or> RPCReply send rcv rst p)"
 
   RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
                            Init RPCInit rcv rst p
-                         & \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
-                         & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
+                         \<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
+                         \<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
 
   RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
 
@@ -84,7 +84,7 @@
 lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: Return_def RPC_action_defs)
 
-lemma RPCbusy: "\<turnstile> $(Calling rcv p) & $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
+lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
   by (auto simp: RPC_action_defs)
 
 (* RPC failure actions are visible. *)
@@ -98,13 +98,13 @@
 
 (* Enabledness of some actions *)
 lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
-    \<turnstile> \<not>Calling rcv p & Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
+    \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
     [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
 
 lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
-      \<turnstile> \<not>Calling rcv p & Calling send p & rst!p = #rpcB  
+      \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
          \<longrightarrow> Enabled (RPCReply send rcv rst p)"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
diff -r 479071e8778f -r e0b77517f9a9 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Fri Jun 26 15:03:54 2015 +0200
+++ b/src/HOL/TLA/TLA.thy	Fri Jun 26 15:55:44 2015 +0200
@@ -24,15 +24,15 @@
 
   (** concrete syntax **)
 syntax
-  "_Box"     :: "lift \<Rightarrow> lift"                        ("([]_)" [40] 40)
-  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(<>_)" [40] 40)
-  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ ~> _)" [23,22] 22)
+  "_Box"     :: "lift \<Rightarrow> lift"                        ("(\<box>_)" [40] 40)
+  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(\<diamond>_)" [40] 40)
+  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ \<leadsto> _)" [23,22] 22)
   "_stable"  :: "lift \<Rightarrow> lift"                        ("(stable/ _)")
   "_WF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(WF'(_')'_(_))" [0,60] 55)
   "_SF"      :: "[lift,lift] \<Rightarrow> lift"                 ("(SF'(_')'_(_))" [0,60] 55)
 
-  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3EEX _./ _)" [0,10] 10)
-  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3AALL _./ _)" [0,10] 10)
+  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
+  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
 
 translations
   "_Box"      ==   "CONST Box"
@@ -44,21 +44,14 @@
   "_EEx v A"  ==   "Eex v. A"
   "_AAll v A" ==   "Aall v. A"
 
-  "sigma |= []F"         <= "_Box F sigma"
-  "sigma |= <>F"         <= "_Dmd F sigma"
-  "sigma |= F ~> G"      <= "_leadsto F G sigma"
-  "sigma |= stable P"    <= "_stable P sigma"
-  "sigma |= WF(A)_v"     <= "_WF A v sigma"
-  "sigma |= SF(A)_v"     <= "_SF A v sigma"
-  "sigma |= EEX x. F"    <= "_EEx x F sigma"
-  "sigma |= AALL x. F"    <= "_AAll x F sigma"
-
-syntax (xsymbols)
-  "_Box"     :: "lift \<Rightarrow> lift"                        ("(\<box>_)" [40] 40)
-  "_Dmd"     :: "lift \<Rightarrow> lift"                        ("(\<diamond>_)" [40] 40)
-  "_leadsto" :: "[lift,lift] \<Rightarrow> lift"                 ("(_ \<leadsto> _)" [23,22] 22)
-  "_EEx"     :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>\<exists> _./ _)" [0,10] 10)
-  "_AAll"    :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>\<forall> _./ _)" [0,10] 10)
+  "sigma \<Turnstile> \<box>F"         <= "_Box F sigma"
+  "sigma \<Turnstile> \<diamond>F"         <= "_Dmd F sigma"
+  "sigma \<Turnstile> F \<leadsto> G"      <= "_leadsto F G sigma"
+  "sigma \<Turnstile> stable P"    <= "_stable P sigma"
+  "sigma \<Turnstile> WF(A)_v"     <= "_WF A v sigma"
+  "sigma \<Turnstile> SF(A)_v"     <= "_SF A v sigma"
+  "sigma \<Turnstile> \<exists>\<exists>x. F"    <= "_EEx x F sigma"
+  "sigma \<Turnstile> \<forall>\<forall>x. F"    <= "_AAll x F sigma"
 
 axiomatization where
   (* Definitions of derived operators *)
@@ -77,11 +70,11 @@
   normalT:    "\<And>F G. \<turnstile> \<box>(F \<longrightarrow> G) \<longrightarrow> (\<box>F \<longrightarrow> \<box>G)" and    (* polymorphic *)
   reflT:      "\<And>F. \<turnstile> \<box>F \<longrightarrow> F" and         (* F::temporal *)
   transT:     "\<And>F. \<turnstile> \<box>F \<longrightarrow> \<box>\<box>F" and     (* polymorphic *)
-  linT:       "\<And>F G. \<turnstile> \<diamond>F & \<diamond>G \<longrightarrow> (\<diamond>(F & \<diamond>G)) | (\<diamond>(G & \<diamond>F))" and
-  discT:      "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F & \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
+  linT:       "\<And>F G. \<turnstile> \<diamond>F \<and> \<diamond>G \<longrightarrow> (\<diamond>(F \<and> \<diamond>G)) \<or> (\<diamond>(G \<and> \<diamond>F))" and
+  discT:      "\<And>F. \<turnstile> \<box>(F \<longrightarrow> \<diamond>(\<not>F \<and> \<diamond>F)) \<longrightarrow> (F \<longrightarrow> \<box>\<diamond>F)" and
   primeI:     "\<And>P. \<turnstile> \<box>P \<longrightarrow> Init P`" and
   primeE:     "\<And>P F. \<turnstile> \<box>(Init P \<longrightarrow> \<box>F) \<longrightarrow> Init P` \<longrightarrow> (F \<longrightarrow> \<box>F)" and
-  indT:       "\<And>P F. \<turnstile> \<box>(Init P & \<not>\<box>F \<longrightarrow> Init P` & F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
+  indT:       "\<And>P F. \<turnstile> \<box>(Init P \<and> \<not>\<box>F \<longrightarrow> Init P` \<and> F) \<longrightarrow> Init P \<longrightarrow> \<box>F" and
   allT:       "\<And>F. \<turnstile> (\<forall>x. \<box>(F x)) = (\<box>(\<forall> x. F x))"
 
 axiomatization where
@@ -93,7 +86,7 @@
   eexE:       "\<lbrakk> sigma \<Turnstile> (\<exists>\<exists>x. F x); basevars vs;
                  (\<And>x. \<lbrakk> basevars (x, vs); sigma \<Turnstile> F x \<rbrakk> \<Longrightarrow> (G sigma)::bool)
               \<rbrakk> \<Longrightarrow> G sigma" and
-  history:    "\<turnstile> \<exists>\<exists>h. Init(h = ha) & \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
+  history:    "\<turnstile> \<exists>\<exists>h. Init(h = ha) \<and> \<box>(\<forall>x. $h = #x \<longrightarrow> h` = hb x)"
 
 
 (* Specialize intensional introduction/elimination rules for temporal formulas *)
@@ -255,9 +248,9 @@
   by (erule (1) DmdImpl [temp_use])
 
 (* ------------------------ STL5 ------------------------------------------- *)
-lemma STL5: "\<turnstile> (\<box>F & \<box>G) = (\<box>(F & G))"
+lemma STL5: "\<turnstile> (\<box>F \<and> \<box>G) = (\<box>(F \<and> G))"
   apply auto
-  apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F & G))")
+  apply (subgoal_tac "sigma \<Turnstile> \<box> (G \<longrightarrow> (F \<and> G))")
      apply (erule normalT [temp_use])
      apply (fastforce elim!: STL4E [temp_use])+
   done
@@ -273,7 +266,7 @@
 lemma box_conjE:
   assumes "sigma \<Turnstile> \<box>F"
      and "sigma \<Turnstile> \<box>G"
-  and "sigma \<Turnstile> \<box>(F&G) \<Longrightarrow> PROP R"
+  and "sigma \<Turnstile> \<box>(F\<and>G) \<Longrightarrow> PROP R"
   shows "PROP R"
   by (rule assms STL5 [temp_unlift, THEN iffD1] conjI)+
 
@@ -317,7 +310,7 @@
 *)
 lemmas all_box = allT [temp_unlift, symmetric]
 
-lemma DmdOr: "\<turnstile> (\<diamond>(F | G)) = (\<diamond>F | \<diamond>G)"
+lemma DmdOr: "\<turnstile> (\<diamond>(F \<or> G)) = (\<diamond>F \<or> \<diamond>G)"
   apply (auto simp add: dmd_def split_box_conj [try_rewrite])
   apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
   done
@@ -327,7 +320,7 @@
 
 lemmas ex_dmd = exT [temp_unlift, symmetric]
 
-lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F & \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
+lemma STL4Edup: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>A; sigma \<Turnstile> \<box>F; \<turnstile> F \<and> \<box>A \<longrightarrow> G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>G"
   apply (erule dup_boxE)
   apply merge_box
   apply (erule STL4E)
@@ -346,7 +339,7 @@
 lemma InfImpl:
   assumes 1: "sigma \<Turnstile> \<box>\<diamond>F"
     and 2: "sigma \<Turnstile> \<box>G"
-    and 3: "\<turnstile> F & G \<longrightarrow> H"
+    and 3: "\<turnstile> F \<and> G \<longrightarrow> H"
   shows "sigma \<Turnstile> \<box>\<diamond>H"
   apply (insert 1 2)
   apply (erule_tac F = G in dup_boxE)
@@ -356,7 +349,7 @@
 
 (* ------------------------ STL6 ------------------------------------------- *)
 (* Used in the proof of STL6, but useful in itself. *)
-lemma BoxDmd: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(\<box>F & G)"
+lemma BoxDmd: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(\<box>F \<and> G)"
   apply (unfold dmd_def)
   apply clarsimp
   apply (erule dup_boxE)
@@ -366,14 +359,14 @@
   done
 
 (* weaker than BoxDmd, but more polymorphic (and often just right) *)
-lemma BoxDmd_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(F & G)"
+lemma BoxDmd_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(F \<and> G)"
   apply (unfold dmd_def)
   apply clarsimp
   apply merge_box
   apply (fastforce elim!: notE STL4E [temp_use])
   done
 
-lemma BoxDmd2_simple: "\<turnstile> \<box>F & \<diamond>G \<longrightarrow> \<diamond>(G & F)"
+lemma BoxDmd2_simple: "\<turnstile> \<box>F \<and> \<diamond>G \<longrightarrow> \<diamond>(G \<and> F)"
   apply (unfold dmd_def)
   apply clarsimp
   apply merge_box
@@ -383,13 +376,13 @@
 lemma DmdImpldup:
   assumes 1: "sigma \<Turnstile> \<box>A"
     and 2: "sigma \<Turnstile> \<diamond>F"
-    and 3: "\<turnstile> \<box>A & F \<longrightarrow> G"
+    and 3: "\<turnstile> \<box>A \<and> F \<longrightarrow> G"
   shows "sigma \<Turnstile> \<diamond>G"
   apply (rule 2 [THEN 1 [THEN BoxDmd [temp_use]], THEN DmdImplE])
   apply (rule 3)
   done
 
-lemma STL6: "\<turnstile> \<diamond>\<box>F & \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F & G)"
+lemma STL6: "\<turnstile> \<diamond>\<box>F \<and> \<diamond>\<box>G \<longrightarrow> \<diamond>\<box>(F \<and> G)"
   apply (auto simp: STL5 [temp_rewrite, symmetric])
   apply (drule linT [temp_use])
    apply assumption
@@ -444,7 +437,7 @@
 lemma BoxDmdBox: "\<turnstile> (\<box>\<diamond>\<box>F) = (\<diamond>\<box>F)"
   apply (auto dest!: STL2 [temp_use])
   apply (rule ccontr)
-  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F & \<diamond>\<box>\<not>\<box>F")
+  apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>\<box>F \<and> \<diamond>\<box>\<not>\<box>F")
    apply (erule thin_rl)
    apply auto
     apply (drule STL6 [temp_use])
@@ -463,7 +456,7 @@
 
 (* ------------------------ Miscellaneous ----------------------------------- *)
 
-lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F | \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F | G)"
+lemma BoxOr: "\<And>sigma. \<lbrakk> sigma \<Turnstile> \<box>F \<or> \<box>G \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>(F \<or> G)"
   by (fastforce elim!: STL4E [temp_use])
 
 (* "persistently implies infinitely often" *)
@@ -476,7 +469,7 @@
   apply simp
   done
 
-lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F & \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F & G)"
+lemma BoxDmdDmdBox: "\<turnstile> \<box>\<diamond>F \<and> \<diamond>\<box>G \<longrightarrow> \<box>\<diamond>(F \<and> G)"
   apply clarsimp
   apply (rule ccontr)
   apply (unfold more_temp_simps2)
@@ -494,11 +487,11 @@
 section "priming"
 
 (* ------------------------ TLA2 ------------------------------------------- *)
-lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P & Init P`"
+lemma STL2_pr: "\<turnstile> \<box>P \<longrightarrow> Init P \<and> Init P`"
   by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
 
 (* Auxiliary lemma allows priming of boxed actions *)
-lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P & P$)"
+lemma BoxPrime: "\<turnstile> \<box>P \<longrightarrow> \<box>($P \<and> P$)"
   apply clarsimp
   apply (erule dup_boxE)
   apply (unfold boxInit_act)
@@ -507,7 +500,7 @@
   done
 
 lemma TLA2:
-  assumes "\<turnstile> $P & P$ \<longrightarrow> A"
+  assumes "\<turnstile> $P \<and> P$ \<longrightarrow> A"
   shows "\<turnstile> \<box>P \<longrightarrow> \<box>A"
   apply clarsimp
   apply (drule BoxPrime [temp_use])
@@ -515,7 +508,7 @@
     elim!: STL4E [temp_use])
   done
 
-lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P & P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
+lemma TLA2E: "\<lbrakk> sigma \<Turnstile> \<box>P; \<turnstile> $P \<and> P$ \<longrightarrow> A \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>A"
   by (erule (1) TLA2 [temp_use])
 
 lemma DmdPrime: "\<turnstile> (\<diamond>P`) \<longrightarrow> (\<diamond>P)"
@@ -529,7 +522,7 @@
 section "stable, invariant"
 
 lemma ind_rule:
-   "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P & \<not>\<box>F \<longrightarrow> Init(P`) & F) \<rbrakk>
+   "\<lbrakk> sigma \<Turnstile> \<box>H; sigma \<Turnstile> Init P; \<turnstile> H \<longrightarrow> (Init P \<and> \<not>\<box>F \<longrightarrow> Init(P`) \<and> F) \<rbrakk>
     \<Longrightarrow> sigma \<Turnstile> \<box>F"
   apply (rule indT [temp_use])
    apply (erule (2) STL4E)
@@ -552,12 +545,12 @@
   done
 
 lemma StableT:
-    "\<And>P. \<turnstile> $P & A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
+    "\<And>P. \<turnstile> $P \<and> A \<longrightarrow> P` \<Longrightarrow> \<turnstile> \<box>A \<longrightarrow> stable P"
   apply (unfold stable_def)
   apply (fastforce elim!: STL4E [temp_use])
   done
 
-lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P & A --> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
+lemma Stable: "\<lbrakk> sigma \<Turnstile> \<box>A; \<turnstile> $P \<and> A \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> stable P"
   by (erule (1) StableT [temp_use])
 
 (* Generalization of INV1 *)
@@ -568,7 +561,7 @@
   apply (force simp: stable_def elim: STL4E [temp_use] INV1 [temp_use])
   done
 
-lemma DmdStable: "\<turnstile> (stable P) & \<diamond>P \<longrightarrow> \<diamond>\<box>P"
+lemma DmdStable: "\<turnstile> (stable P) \<and> \<diamond>P \<longrightarrow> \<diamond>\<box>P"
   apply clarsimp
   apply (rule DmdImpl2)
    prefer 2
@@ -609,7 +602,7 @@
   Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
 *}
 
-lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` | Q`) \<longrightarrow> (stable P) | \<diamond>Q"
+lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q"
   apply (unfold dmd_def)
   apply (clarsimp dest!: BoxPrime [temp_use])
   apply merge_box
@@ -622,13 +615,13 @@
 section "recursive expansions"
 
 (* Recursive expansions of \<box> and \<diamond> for state predicates *)
-lemma BoxRec: "\<turnstile> (\<box>P) = (Init P & \<box>P`)"
+lemma BoxRec: "\<turnstile> (\<box>P) = (Init P \<and> \<box>P`)"
   apply (auto intro!: STL2_gen [temp_use])
    apply (fastforce elim!: TLA2E [temp_use])
   apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
   done
 
-lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P | \<diamond>P`)"
+lemma DmdRec: "\<turnstile> (\<diamond>P) = (Init P \<or> \<diamond>P`)"
   apply (unfold dmd_def BoxRec [temp_rewrite])
   apply (auto simp: Init_simps)
   done
@@ -643,7 +636,7 @@
    apply (rule DBImplBD [temp_use])
    apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box>P")
     apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
-   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P & \<box>\<not>P`)")
+   apply (subgoal_tac "sigma \<Turnstile> \<diamond>\<box> (\<diamond>P \<and> \<box>\<not>P`)")
     apply (force simp: boxInit_stp [temp_use]
       elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
    apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
@@ -651,7 +644,7 @@
   done
 
 lemma InfiniteEnsures:
-  "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A & N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
+  "\<lbrakk> sigma \<Turnstile> \<box>N; sigma \<Turnstile> \<box>\<diamond>A; \<turnstile> A \<and> N \<longrightarrow> P` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>P"
   apply (unfold InfinitePrime [temp_rewrite])
   apply (rule InfImpl)
     apply assumption+
@@ -661,12 +654,12 @@
 section "fairness"
 
 (* alternative definitions of fairness *)
-lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
+lemma WF_alt: "\<turnstile> WF(A)_v = (\<box>\<diamond>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
   apply (unfold WF_def dmd_def)
   apply fastforce
   done
 
-lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) | \<box>\<diamond><A>_v)"
+lemma SF_alt: "\<turnstile> SF(A)_v = (\<diamond>\<box>\<not>Enabled(<A>_v) \<or> \<box>\<diamond><A>_v)"
   apply (unfold SF_def dmd_def)
   apply fastforce
   done
@@ -702,7 +695,7 @@
 
 section "\<leadsto>"
 
-lemma leadsto_init: "\<turnstile> (Init F) & (F \<leadsto> G) \<longrightarrow> \<diamond>G"
+lemma leadsto_init: "\<turnstile> (Init F) \<and> (F \<leadsto> G) \<longrightarrow> \<diamond>G"
   apply (unfold leadsto_def)
   apply (auto dest!: STL2 [temp_use])
   done
@@ -723,7 +716,7 @@
   apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
   done
 
-lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F & (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
+lemma leadsto_infinite: "\<turnstile> \<box>\<diamond>F \<and> (F \<leadsto> G) \<longrightarrow> \<box>\<diamond>G"
   apply clarsimp
   apply (erule InitDmd [temp_use, THEN streett_leadsto [temp_unlift, THEN iffD2, THEN mp]])
   apply (simp add: dmdInitD)
@@ -743,7 +736,7 @@
 (* introduce an invariant into the proof of a leadsto assertion.
    \<box>I \<longrightarrow> ((P \<leadsto> Q)  =  (P /\ I \<leadsto> Q))
 *)
-lemma INV_leadsto: "\<turnstile> \<box>I & (P & I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
+lemma INV_leadsto: "\<turnstile> \<box>I \<and> (P \<and> I \<leadsto> Q) \<longrightarrow> (P \<leadsto> Q)"
   apply (unfold leadsto_def)
   apply clarsimp
   apply (erule STL4Edup)
@@ -751,12 +744,12 @@
   apply (auto simp: Init_simps dest!: STL2_gen [temp_use])
   done
 
-lemma leadsto_classical: "\<turnstile> (Init F & \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
+lemma leadsto_classical: "\<turnstile> (Init F \<and> \<box>\<not>G \<leadsto> G) \<longrightarrow> (F \<leadsto> G)"
   apply (unfold leadsto_def dmd_def)
   apply (force simp: Init_simps elim!: STL4E [temp_use])
   done
 
-lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>~F)"
+lemma leadsto_false: "\<turnstile> (F \<leadsto> #False) = (\<box>\<not>F)"
   apply (unfold leadsto_def)
   apply (simp add: boxNotInitD)
   done
@@ -781,7 +774,7 @@
   by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
 
 lemma EnsuresLeadsto:
-  assumes "\<turnstile> A & $P \<longrightarrow> Q`"
+  assumes "\<turnstile> A \<and> $P \<longrightarrow> Q`"
   shows "\<turnstile> \<box>A \<longrightarrow> (P \<leadsto> Q)"
   apply (unfold leadsto_def)
   apply (clarsimp elim!: INV_leadsto [temp_use])
@@ -797,15 +790,15 @@
   done
 
 lemma ensures:
-  assumes 1: "\<turnstile> $P & N \<longrightarrow> P` | Q`"
-    and 2: "\<turnstile> ($P & N) & A \<longrightarrow> Q`"
-  shows "\<turnstile> \<box>N & \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
+  assumes 1: "\<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`"
+    and 2: "\<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`"
+  shows "\<turnstile> \<box>N \<and> \<box>(\<box>P \<longrightarrow> \<diamond>A) \<longrightarrow> (P \<leadsto> Q)"
   apply (unfold leadsto_def)
   apply clarsimp
   apply (erule STL4Edup)
    apply assumption
   apply clarsimp
-  apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` | Q`) ")
+  apply (subgoal_tac "sigmaa \<Turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) ")
    apply (drule unless [temp_use])
    apply (clarsimp dest!: INV1 [temp_use])
   apply (rule 2 [THEN DmdImpl, temp_use, THEN DmdPrime [temp_use]])
@@ -815,16 +808,16 @@
   done
 
 lemma ensures_simple:
-  "\<lbrakk> \<turnstile> $P & N \<longrightarrow> P` | Q`;
-      \<turnstile> ($P & N) & A \<longrightarrow> Q`
-   \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N & \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
+  "\<lbrakk> \<turnstile> $P \<and> N \<longrightarrow> P` \<or> Q`;
+      \<turnstile> ($P \<and> N) \<and> A \<longrightarrow> Q`
+   \<rbrakk> \<Longrightarrow> \<turnstile> \<box>N \<and> \<box>\<diamond>A \<longrightarrow> (P \<leadsto> Q)"
   apply clarsimp
   apply (erule (2) ensures [temp_use])
   apply (force elim!: STL4E [temp_use])
   done
 
 lemma EnsuresInfinite:
-    "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A & $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
+    "\<lbrakk> sigma \<Turnstile> \<box>\<diamond>P; sigma \<Turnstile> \<box>A; \<turnstile> A \<and> $P \<longrightarrow> Q` \<rbrakk> \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>Q"
   apply (erule leadsto_infinite [temp_use])
   apply (erule EnsuresLeadsto [temp_use])
   apply assumption
@@ -839,7 +832,7 @@
   apply (rule necT InitDmd_gen)+
   done
 
-lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) & (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
+lemma LatticeTransitivity: "\<turnstile> (G \<leadsto> H) \<and> (F \<leadsto> G) \<longrightarrow> (F \<leadsto> H)"
   apply (unfold leadsto_def)
   apply clarsimp
   apply (erule dup_boxE) (* \<box>\<box>(Init G \<longrightarrow> H) *)
@@ -852,47 +845,47 @@
   apply (simp add: dmdInitD)
   done
 
-lemma LatticeDisjunctionElim1: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
+lemma LatticeDisjunctionElim1: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (F \<leadsto> H)"
   apply (unfold leadsto_def)
   apply (auto simp: Init_simps elim!: STL4E [temp_use])
   done
 
-lemma LatticeDisjunctionElim2: "\<turnstile> (F | G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
+lemma LatticeDisjunctionElim2: "\<turnstile> (F \<or> G \<leadsto> H) \<longrightarrow> (G \<leadsto> H)"
   apply (unfold leadsto_def)
   apply (auto simp: Init_simps elim!: STL4E [temp_use])
   done
 
-lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) & (G \<leadsto> H) \<longrightarrow> (F | G \<leadsto> H)"
+lemma LatticeDisjunctionIntro: "\<turnstile> (F \<leadsto> H) \<and> (G \<leadsto> H) \<longrightarrow> (F \<or> G \<leadsto> H)"
   apply (unfold leadsto_def)
   apply clarsimp
   apply merge_box
   apply (auto simp: Init_simps elim!: STL4E [temp_use])
   done
 
-lemma LatticeDisjunction: "\<turnstile> (F | G \<leadsto> H) = ((F \<leadsto> H) & (G \<leadsto> H))"
+lemma LatticeDisjunction: "\<turnstile> (F \<or> G \<leadsto> H) = ((F \<leadsto> H) \<and> (G \<leadsto> H))"
   by (auto intro: LatticeDisjunctionIntro [temp_use]
     LatticeDisjunctionElim1 [temp_use]
     LatticeDisjunctionElim2 [temp_use])
 
-lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B | C) & (B \<leadsto> D) & (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeDiamond: "\<turnstile> (A \<leadsto> B \<or> C) \<and> (B \<leadsto> D) \<and> (C \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   apply clarsimp
-  apply (subgoal_tac "sigma \<Turnstile> (B | C) \<leadsto> D")
-  apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
+  apply (subgoal_tac "sigma \<Turnstile> (B \<or> C) \<leadsto> D")
+  apply (erule_tac G = "LIFT (B \<or> C)" in LatticeTransitivity [temp_use])
    apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
   done
 
-lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D | B) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeTriangle: "\<turnstile> (A \<leadsto> D \<or> B) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   apply clarsimp
-  apply (subgoal_tac "sigma \<Turnstile> (D | B) \<leadsto> D")
-   apply (erule_tac G = "LIFT (D | B)" in LatticeTransitivity [temp_use])
+  apply (subgoal_tac "sigma \<Turnstile> (D \<or> B) \<leadsto> D")
+   apply (erule_tac G = "LIFT (D \<or> B)" in LatticeTransitivity [temp_use])
   apply assumption
   apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
   done
 
-lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B | D) & (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
+lemma LatticeTriangle2: "\<turnstile> (A \<leadsto> B \<or> D) \<and> (B \<leadsto> D) \<longrightarrow> (A \<leadsto> D)"
   apply clarsimp
-  apply (subgoal_tac "sigma \<Turnstile> B | D \<leadsto> D")
-   apply (erule_tac G = "LIFT (B | D)" in LatticeTransitivity [temp_use])
+  apply (subgoal_tac "sigma \<Turnstile> B \<or> D \<leadsto> D")
+   apply (erule_tac G = "LIFT (B \<or> D)" in LatticeTransitivity [temp_use])
    apply assumption
   apply (auto intro: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
   done
@@ -901,10 +894,10 @@
 section "Fairness rules"
 
 lemma WF1:
-  "\<lbrakk> \<turnstile> $P & N  \<longrightarrow> P` | Q`;
-      \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
-      \<turnstile> $P & N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
-  \<Longrightarrow> \<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
+  "\<lbrakk> \<turnstile> $P \<and> N  \<longrightarrow> P` \<or> Q`;
+      \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
+      \<turnstile> $P \<and> N \<longrightarrow> $(Enabled(<A>_v)) \<rbrakk>
+  \<Longrightarrow> \<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> Q)"
   apply (clarsimp dest!: BoxWFI [temp_use])
   apply (erule (2) ensures [temp_use])
   apply (erule (1) STL4Edup)
@@ -917,10 +910,10 @@
 
 (* Sometimes easier to use; designed for action B rather than state predicate Q *)
 lemma WF_leadsto:
-  assumes 1: "\<turnstile> N & $P \<longrightarrow> $Enabled (<A>_v)"
-    and 2: "\<turnstile> N & <A>_v \<longrightarrow> B"
-    and 3: "\<turnstile> \<box>(N & [~A]_v) \<longrightarrow> stable P"
-  shows "\<turnstile> \<box>N & WF(A)_v \<longrightarrow> (P \<leadsto> B)"
+  assumes 1: "\<turnstile> N \<and> $P \<longrightarrow> $Enabled (<A>_v)"
+    and 2: "\<turnstile> N \<and> <A>_v \<longrightarrow> B"
+    and 3: "\<turnstile> \<box>(N \<and> [\<not>A]_v) \<longrightarrow> stable P"
+  shows "\<turnstile> \<box>N \<and> WF(A)_v \<longrightarrow> (P \<leadsto> B)"
   apply (unfold leadsto_def)
   apply (clarsimp dest!: BoxWFI [temp_use])
   apply (erule (1) STL4Edup)
@@ -939,10 +932,10 @@
   done
 
 lemma SF1:
-  "\<lbrakk> \<turnstile> $P & N  \<longrightarrow> P` | Q`;
-      \<turnstile> ($P & N) & <A>_v \<longrightarrow> Q`;
-      \<turnstile> \<box>P & \<box>N & \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
-  \<Longrightarrow> \<turnstile> \<box>N & SF(A)_v & \<box>F \<longrightarrow> (P \<leadsto> Q)"
+  "\<lbrakk> \<turnstile> $P \<and> N  \<longrightarrow> P` \<or> Q`;
+      \<turnstile> ($P \<and> N) \<and> <A>_v \<longrightarrow> Q`;
+      \<turnstile> \<box>P \<and> \<box>N \<and> \<box>F \<longrightarrow> \<diamond>Enabled(<A>_v) \<rbrakk>
+  \<Longrightarrow> \<turnstile> \<box>N \<and> SF(A)_v \<and> \<box>F \<longrightarrow> (P \<leadsto> Q)"
   apply (clarsimp dest!: BoxSFI [temp_use])
   apply (erule (2) ensures [temp_use])
   apply (erule_tac F = F in dup_boxE)
@@ -957,11 +950,11 @@
   done
 
 lemma WF2:
-  assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
-    and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
-    and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
-    and 4: "\<turnstile> \<box>(N & [~B]_f) & WF(A)_f & \<box>F & \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
-  shows "\<turnstile> \<box>N & WF(A)_f & \<box>F \<longrightarrow> WF(M)_g"
+  assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
+    and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
+    and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
+    and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> WF(A)_f \<and> \<box>F \<and> \<diamond>\<box>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
+  shows "\<turnstile> \<box>N \<and> WF(A)_f \<and> \<box>F \<longrightarrow> WF(M)_g"
   apply (clarsimp dest!: BoxWFI [temp_use] BoxDmdBox [temp_use, THEN iffD2]
     simp: WF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
@@ -970,7 +963,7 @@
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   apply (rule classical)
-  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
+  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
@@ -982,7 +975,7 @@
   apply (erule_tac V = "sigmaa \<Turnstile> \<diamond>\<box>P" in thin_rl)
   apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
   apply (drule BoxWFI [temp_use])
-  apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
+  apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
   apply merge_temp_box
   apply (erule DmdImpldup)
    apply assumption
@@ -995,11 +988,11 @@
   done
 
 lemma SF2:
-  assumes 1: "\<turnstile> N & <B>_f \<longrightarrow> <M>_g"
-    and 2: "\<turnstile> $P & P` & <N & A>_f \<longrightarrow> B"
-    and 3: "\<turnstile> P & Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
-    and 4: "\<turnstile> \<box>(N & [~B]_f) & SF(A)_f & \<box>F & \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
-  shows "\<turnstile> \<box>N & SF(A)_f & \<box>F \<longrightarrow> SF(M)_g"
+  assumes 1: "\<turnstile> N \<and> <B>_f \<longrightarrow> <M>_g"
+    and 2: "\<turnstile> $P \<and> P` \<and> <N \<and> A>_f \<longrightarrow> B"
+    and 3: "\<turnstile> P \<and> Enabled(<M>_g) \<longrightarrow> Enabled(<A>_f)"
+    and 4: "\<turnstile> \<box>(N \<and> [\<not>B]_f) \<and> SF(A)_f \<and> \<box>F \<and> \<box>\<diamond>Enabled(<M>_g) \<longrightarrow> \<diamond>\<box>P"
+  shows "\<turnstile> \<box>N \<and> SF(A)_f \<and> \<box>F \<longrightarrow> SF(M)_g"
   apply (clarsimp dest!: BoxSFI [temp_use] simp: 2 [try_rewrite] SF_def [where A = M])
   apply (erule_tac F = F in dup_boxE)
   apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g) " in dup_boxE)
@@ -1008,7 +1001,7 @@
    apply assumption
   apply (clarsimp intro!: BoxDmd_simple [temp_use, THEN 1 [THEN DmdImpl, temp_use]])
   apply (rule classical)
-  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P & P` & N) & <A>_f)")
+  apply (subgoal_tac "sigmaa \<Turnstile> \<diamond> (($P \<and> P` \<and> N) \<and> <A>_f)")
    apply (force simp: angle_def intro!: 2 [temp_use] elim!: DmdImplE [temp_use])
   apply (rule BoxDmd_simple [THEN DmdImpl, unfolded DmdDmd [temp_rewrite], temp_use])
   apply (simp add: NotDmd [temp_use] not_angle [try_rewrite])
@@ -1018,7 +1011,7 @@
   apply (erule_tac V = "sigmaa \<Turnstile> \<box>F" in thin_rl)
   apply (drule BoxSFI [temp_use])
   apply (erule_tac F = "TEMP \<diamond>Enabled (<M>_g)" in dup_boxE)
-  apply (erule_tac F = "ACT N & [~B]_f" in dup_boxE)
+  apply (erule_tac F = "ACT N \<and> [\<not>B]_f" in dup_boxE)
   apply merge_temp_box
   apply (erule DmdImpldup)
    apply assumption
@@ -1037,19 +1030,19 @@
 
 lemma wf_leadsto:
   assumes 1: "wf r"
-    and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G | (\<exists>y. #((y,x):r) & F y))    "
+    and 2: "\<And>x. sigma \<Turnstile> F x \<leadsto> (G \<or> (\<exists>y. #((y,x)\<in>r) \<and> F y))    "
   shows "sigma \<Turnstile> F x \<leadsto> G"
   apply (rule 1 [THEN wf_induct])
   apply (rule LatticeTriangle [temp_use])
    apply (rule 2)
   apply (auto simp: leadsto_exists [try_rewrite])
-  apply (case_tac "(y,x) :r")
+  apply (case_tac "(y,x) \<in> r")
    apply force
   apply (force simp: leadsto_def Init_simps intro!: necT [temp_use])
   done
 
 (* If r is well-founded, state function v cannot decrease forever *)
-lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) : #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
+lemma wf_not_box_decrease: "\<And>r. wf r \<Longrightarrow> \<turnstile> \<box>[ (v`, $v) \<in> #r ]_v \<longrightarrow> \<diamond>\<box>[#False]_v"
   apply clarsimp
   apply (rule ccontr)
   apply (subgoal_tac "sigma \<Turnstile> (\<exists>x. v=#x) \<leadsto> #False")
@@ -1070,7 +1063,7 @@
 *)
 lemma wf_box_dmd_decrease:
   assumes 1: "wf r"
-  shows "\<turnstile> \<box>\<diamond>((v`, $v) : #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
+  shows "\<turnstile> \<box>\<diamond>((v`, $v) \<in> #r) \<longrightarrow> \<box>\<diamond><(v`, $v) \<notin> #r>_v"
   apply clarsimp
   apply (rule ccontr)
   apply (simp add: not_angle [try_rewrite] more_temp_simps)
@@ -1089,7 +1082,7 @@
 *)
 lemma nat_box_dmd_decrease: "\<And>n::nat stfun. \<turnstile> \<box>\<diamond>(n` < $n) \<longrightarrow> \<box>\<diamond>($n < n`)"
   apply clarsimp
-  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><~ ((n`,$n) : #less_than) >_n")
+  apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond><\<not> ((n`,$n) \<in> #less_than)>_n")
    apply (erule thin_rl)
    apply (erule STL4E)
    apply (rule DmdImpl)
@@ -1141,9 +1134,9 @@
   assumes 1: "sigma \<Turnstile> Init I"
     and 2: "sigma \<Turnstile> \<box>N"
     and 3: "basevars vs"
-    and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I & h = ha \<longrightarrow> HI h"
+    and 4: "\<And>h. basevars(h,vs) \<Longrightarrow> \<turnstile> I \<and> h = ha \<longrightarrow> HI h"
     and 5: "\<And>h s t. \<lbrakk> basevars(h,vs); N (s,t); h t = hb (h s) (s,t) \<rbrakk> \<Longrightarrow> HN h (s,t)"
-  shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) & \<box>(HN h)"
+  shows "sigma \<Turnstile> \<exists>\<exists>h. Init (HI h) \<and> \<box>(HN h)"
   apply (rule history [temp_use, THEN eexE])
   apply (rule 3)
   apply (rule eexI [temp_use])
@@ -1161,7 +1154,7 @@
    example of a history variable: existence of a clock
 *)
 
-lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) & \<box>(h` = (~$h))"
+lemma "\<turnstile> \<exists>\<exists>h. Init(h = #True) \<and> \<box>(h` = (\<not>$h))"
   apply (rule tempI)
   apply (rule historyI)
   apply (force simp: Init_defs intro!: unit_base [temp_use] necT [temp_use])+