diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 11:44:22 2015 +0200
@@ -63,7 +63,7 @@
 definition
   (* the environment action *)
   ENext         :: "PrIds => action"
-  where "ENext p = ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
+  where "ENext p = ACT (\<exists>l. #l : #MemLoc & Call memCh p #(read l))"
 
 
 definition
@@ -83,24 +83,24 @@
 definition
   HistP         :: "histType => PrIds => temporal"
   where "HistP rmhist p = (TEMP Init HInit rmhist p
-                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p))"
+                           & \<box>[HNext rmhist p]_(c p,r p,m p, rmhist!p))"
 
 definition
   Hist          :: "histType => temporal"
-  where "Hist rmhist = TEMP (ALL p. HistP rmhist p)"
+  where "Hist rmhist = TEMP (\<forall>p. HistP rmhist p)"
 
 definition
   (* the implementation *)
   IPImp          :: "PrIds => temporal"
-  where "IPImp p = (TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
+  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
-                       & (ALL l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
+                       & (\<forall>l. #l : #MemLoc --> MSpec rmCh mm ires l)))"
 
 definition
   ImpInit        :: "PrIds => stpred"
-  where "ImpInit p = PRED (  ~Calling memCh p
+  where "ImpInit p = PRED (  \<not>Calling memCh p
                           & MClkInit crCh cst p
                           & RPCInit rmCh rst p
                           & PInit ires p)"
@@ -122,7 +122,7 @@
 
 definition
   Implementation :: "temporal"
-  where "Implementation = (TEMP ( (ALL p. Init (~Calling memCh p) & [][ENext p]_(e p))
+  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))"
@@ -139,11 +139,11 @@
                 Calling memCh p = #ecalling
               & Calling crCh p  = #ccalling
               & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
-              & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
+              & (\<not> #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
               & Calling rmCh p  = #rcalling
               & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
-              & (~ #rcalling --> ires!p = #NotAResult)
-              & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
+              & (\<not> #rcalling --> ires!p = #NotAResult)
+              & (\<not> #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
               & cst!p = #cs
               & rst!p = #rs
               & (rmhist!p = #hs1 | rmhist!p = #hs2)
@@ -241,9 +241,9 @@
 
 section "History variable"
 
-lemma HistoryLemma: "|- Init(ALL p. ImpInit p) & [](ALL p. ImpNext p)
-         --> (EEX rmhist. Init(ALL p. HInit rmhist p)
-                          & [](ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
+lemma HistoryLemma: "|- Init(\<forall>p. ImpInit p) & \<box>(\<forall>p. ImpNext p)
+         --> (\<exists>\<exists>rmhist. Init(\<forall>p. HInit rmhist p)
+                          & \<box>(\<forall>p. [HNext rmhist p]_(c p, r p, m p, rmhist!p)))"
   apply clarsimp
   apply (rule historyI)
       apply assumption+
@@ -255,7 +255,7 @@
   apply (erule fun_cong)
   done
 
-lemma History: "|- Implementation --> (EEX rmhist. Hist rmhist)"
+lemma History: "|- Implementation --> (\<exists>\<exists>rmhist. Hist rmhist)"
   apply clarsimp
   apply (rule HistoryLemma [temp_use, THEN eex_mono])
     prefer 3
@@ -274,14 +274,14 @@
 
 (* RPCFailure notin MemVals U {OK,BadArg} *)
 
-lemma MVOKBAnotRF: "MVOKBA x ==> x ~= RPCFailure"
+lemma MVOKBAnotRF: "MVOKBA x ==> x \<noteq> RPCFailure"
   apply (unfold MVOKBA_def)
   apply auto
   done
 
 (* NotAResult notin MemVals U {OK,BadArg,RPCFailure} *)
 
-lemma MVOKBARFnotNR: "MVOKBARF x ==> x ~= NotAResult"
+lemma MVOKBARFnotNR: "MVOKBARF x ==> x \<noteq> NotAResult"
   apply (unfold MVOKBARF_def)
   apply auto
   done
@@ -294,32 +294,32 @@
 *)
 
 (* --- not used ---
-lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p &
-    ~S4 rmhist p & ~S5 rmhist p & ~S6 rmhist p"
+lemma S1_excl: "|- S1 rmhist p --> S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p &
+    \<not>S4 rmhist p & \<not>S5 rmhist p & \<not>S6 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 *)
 
-lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & ~S1 rmhist p"
+lemma S2_excl: "|- S2 rmhist p --> S2 rmhist p & \<not>S1 rmhist p"
   by (auto simp: S_def S1_def S2_def)
 
-lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & ~S1 rmhist p & ~S2 rmhist p"
+lemma S3_excl: "|- S3 rmhist p --> S3 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def)
 
-lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & ~S1 rmhist p & ~S2 rmhist p & ~S3 rmhist p"
+lemma S4_excl: "|- S4 rmhist p --> S4 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p & \<not>S3 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def)
 
-lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & ~S1 rmhist p & ~S2 rmhist p
-                         & ~S3 rmhist p & ~S4 rmhist p"
+lemma S5_excl: "|- S5 rmhist p --> S5 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
+                         & \<not>S3 rmhist p & \<not>S4 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def)
 
-lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & ~S1 rmhist p & ~S2 rmhist p
-                         & ~S3 rmhist p & ~S4 rmhist p & ~S5 rmhist p"
+lemma S6_excl: "|- S6 rmhist p --> S6 rmhist p & \<not>S1 rmhist p & \<not>S2 rmhist p
+                         & \<not>S3 rmhist p & \<not>S4 rmhist p & \<not>S5 rmhist p"
   by (auto simp: S_def S1_def S2_def S3_def S4_def S5_def S6_def)
 
 
 (* ==================== Lemmas about the environment ============================== *)
 
-lemma Envbusy: "|- $(Calling memCh p) --> ~ENext p"
+lemma Envbusy: "|- $(Calling memCh p) --> \<not>ENext p"
   by (auto simp: ENext_def Call_def)
 
 (* ==================== Lemmas about the implementation's states ==================== *)
@@ -447,7 +447,7 @@
     @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
 
 lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
-         & HNext rmhist p & (!l. $MemInv mm l)
+         & HNext rmhist p & (\<forall>l. $MemInv mm l)
          --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   by (auto simp: Read_def dest!: S4ReadInner [temp_use])
 
@@ -563,7 +563,7 @@
 (* Figure 16 is a predicate-action diagram for the implementation. *)
 
 lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
+         & \<not>unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
          --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
       (map (temp_elim @{context})
@@ -573,7 +573,7 @@
   done
 
 lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
+         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
          --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
              & unchanged (e p, r p, m p, rmhist!p)"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
@@ -584,7 +584,7 @@
   done
 
 lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-         & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
+         & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
          --> ((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))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
@@ -596,10 +596,10 @@
   done
 
 lemma Step1_2_4: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & ~unchanged (e p, c p, r p, m p, rmhist!p)
-              & $S4 rmhist p & (!l. $(MemInv mm l))
+              & \<not>unchanged (e p, c p, r p, m p, rmhist!p)
+              & $S4 rmhist p & (\<forall>l. $(MemInv mm l))
          --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
-             | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & 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))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
@@ -610,7 +610,7 @@
   done
 
 lemma Step1_2_5: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
+              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
          --> ((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))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
@@ -621,7 +621,7 @@
   done
 
 lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
-              & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
+              & \<not>unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
          --> ((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))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
@@ -694,7 +694,7 @@
   done
 
 lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
-         & unchanged (e p, c p, r p, rmhist!p) & (!l. $(MemInv mm l))
+         & unchanged (e p, c p, r p, rmhist!p) & (\<forall>l. $(MemInv mm l))
          --> Read memCh mm (resbar rmhist) p"
   by (force simp: Read_def elim!: Step1_4_4a1 [temp_use])
 
@@ -816,7 +816,7 @@
 
 (* Steps that leave all variables unchanged are safe, so I may assume
    that some variable changes in the proof that a step is safe. *)
-lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
+lemma unchanged_safe: "|- (\<not>unchanged (e p, c p, r p, m p, rmhist!p)
              --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply (split_idle simp: square_def)
@@ -850,7 +850,7 @@
   done
 
 lemma S4safe: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (!l. $(MemInv mm l))
+         & (\<forall>l. $(MemInv mm l))
          --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (rule unchanged_safeI)
@@ -900,23 +900,23 @@
 *)
 
 lemma S1_RNextdisabled: "|- S1 rmhist p -->
-         ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
+         \<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
     @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
   apply force
   done
 
 lemma S1_Returndisabled: "|- S1 rmhist p -->
-         ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
+         \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
   by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
     @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
 
-lemma RNext_fair: "|- []<>S1 rmhist p
+lemma RNext_fair: "|- \<box>\<diamond>S1 rmhist p
          --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   by (auto simp: WF_alt [try_rewrite] intro!: S1_RNextdisabled [temp_use]
     elim!: STL4E [temp_use] DmdImplE [temp_use])
 
-lemma Return_fair: "|- []<>S1 rmhist p
+lemma Return_fair: "|- \<box>\<diamond>S1 rmhist p
          --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   by (auto simp: WF_alt [try_rewrite]
     intro!: S1_Returndisabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -942,9 +942,9 @@
     apply (simp_all add: S_def S2_def)
   done
 
-lemma S2_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S2_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & WF(MClkFwd memCh crCh cst p)_(c p)
-         --> (S2 rmhist p ~> S3 rmhist p)"
+         --> (S2 rmhist p \<leadsto> S3 rmhist p)"
   by (rule WF1 S2_successors S2MClkFwd_successors S2MClkFwd_enabled)+
 
 (* ------------------------------ State S3 ------------------------------ *)
@@ -969,15 +969,15 @@
    apply (simp_all add: S_def S3_def)
   done
 
-lemma S3_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S3_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & WF(RPCNext crCh rmCh rst p)_(r p)
-         --> (S3 rmhist p ~> S4 rmhist p | S6 rmhist p)"
+         --> (S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p)"
   by (rule WF1 S3_successors S3RPC_successors S3RPC_enabled)+
 
 (* ------------- State S4 -------------------------------------------------- *)
 
 lemma S4_successors: "|- $S4 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-        & (ALL l. $MemInv mm l)
+        & (\<forall>l. $MemInv mm l)
         --> (S4 rmhist p)$ | (S5 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_4 [temp_use])
@@ -986,22 +986,22 @@
 (* --------- State S4a: S4 /\ (ires p = NotAResult) ------------------------ *)
 
 lemma S4a_successors: "|- $(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
+         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (\<forall>l. $MemInv mm l)
          --> (S4 rmhist p & ires!p = #NotAResult)$
-             | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
+             | ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
   apply split_idle
   apply (auto dest!: Step1_2_4 [temp_use])
   done
 
 lemma S4aRNext_successors: "|- ($(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l))
+         & 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)
-         --> ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
+         --> ((S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)$"
   by (auto simp: angle_def
     dest!: Step1_2_4 [temp_use] ReadResult [temp_use] WriteResult [temp_use])
 
 lemma S4aRNext_enabled: "|- $(S4 rmhist p & ires!p = #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
+         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (\<forall>l. $MemInv mm l)
          --> $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: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (ALL l. $MemInv mm l)) & WF(RNext rmCh mm ires p)_(m p)
+lemma S4a_live: "|- \<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)
          --> (S4 rmhist p & ires!p = #NotAResult
-              ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)"
+              \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p)"
   by (rule WF1 S4a_successors S4aRNext_successors S4aRNext_enabled)+
 
 (* ---------- State S4b: S4 /\ (ires p # NotAResult) --------------------------- *)
 
-lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
-         & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
-         --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
+lemma S4b_successors: "|- $(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)
+         --> (S4 rmhist p & ires!p \<noteq> #NotAResult)$ | (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: "|- ($(S4 rmhist p & ires!p ~= #NotAResult)
+lemma S4bReturn_successors: "|- ($(S4 rmhist p & ires!p \<noteq> #NotAResult)
          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (ALL l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
+         & (\<forall>l. $MemInv mm l)) & <MemReturn rmCh ires p>_(m p)
          --> (S5 rmhist p)$"
   by (force simp: angle_def dest!: Step1_2_4 [temp_use] dest: ReturnNotReadWrite [temp_use])
 
-lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
+lemma S4bReturn_enabled: "|- $(S4 rmhist p & ires!p \<noteq> #NotAResult)
          & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
-         & (ALL l. $MemInv mm l)
+         & (\<forall>l. $MemInv mm l)
          --> $Enabled (<MemReturn rmCh ires p>_(m p))"
   apply (auto simp: m_def intro!: MemReturn_enabled [temp_use])
    apply (cut_tac MI_base)
@@ -1040,9 +1040,9 @@
   apply (simp add: S_def S4_def)
   done
 
-lemma S4b_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (!l. $MemInv mm l))
+lemma S4b_live: "|- \<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)
-         --> (S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p)"
+         --> (S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p)"
   by (rule WF1 S4b_successors S4bReturn_successors S4bReturn_enabled)+
 
 (* ------------------------------ State S5 ------------------------------ *)
@@ -1066,9 +1066,9 @@
    apply (simp_all add: S_def S5_def)
   done
 
-lemma S5_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
+lemma S5_live: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p))
          & WF(RPCNext crCh rmCh rst p)_(r p)
-         --> (S5 rmhist p ~> S6 rmhist p)"
+         --> (S5 rmhist p \<leadsto> S6 rmhist p)"
   by (rule WF1 S5_successors S5RPC_successors S5RPC_enabled)+
 
 (* ------------------------------ State S6 ------------------------------ *)
@@ -1099,11 +1099,11 @@
       addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
   done
 
-lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
-         & SF(MClkReply memCh crCh cst p)_(c p) & []<>(S6 rmhist p)
-         --> []<>(S1 rmhist p)"
+lemma S6_live: "|- \<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)
+         --> \<box>\<diamond>(S1 rmhist p)"
   apply clarsimp
-  apply (subgoal_tac "sigma |= []<> (<MClkReply memCh crCh cst p>_ (c p))")
+  apply (subgoal_tac "sigma |= \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
    apply (erule InfiniteEnsures)
     apply assumption
    apply (tactic {* action_simp_tac @{context} []
@@ -1115,26 +1115,26 @@
 
 (* --------------- aggregate leadsto properties----------------------------- *)
 
-lemma S5S6LeadstoS6: "sigma |= S5 rmhist p ~> S6 rmhist p
-      ==> sigma |= (S5 rmhist p | S6 rmhist p) ~> S6 rmhist p"
+lemma S5S6LeadstoS6: "sigma |= S5 rmhist p \<leadsto> S6 rmhist p
+      ==> sigma |= (S5 rmhist p | S6 rmhist p) \<leadsto> S6 rmhist p"
   by (auto intro!: LatticeDisjunctionIntro [temp_use] LatticeReflexivity [temp_use])
 
-lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
-         sigma |= S5 rmhist p ~> S6 rmhist p |]
-      ==> sigma |= (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p
-                    ~> S6 rmhist p"
+lemma S4bS5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
+      ==> sigma |= (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | S6 rmhist p
+                    \<leadsto> S6 rmhist p"
   by (auto intro!: LatticeDisjunctionIntro [temp_use]
     S5S6LeadstoS6 [temp_use] intro: LatticeTransitivity [temp_use])
 
 lemma S4S5S6LeadstoS6: "[| sigma |= S4 rmhist p & ires!p = #NotAResult
-                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
-         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
-         sigma |= S5 rmhist p ~> S6 rmhist p |]
-      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
+                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
+         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
+      ==> sigma |= S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
   apply (subgoal_tac "sigma |= (S4 rmhist p & ires!p = #NotAResult) |
-    (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p | S6 rmhist p ~> S6 rmhist p")
+    (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 ~= #NotAResult) | S5 rmhist p | S6 rmhist p)" in
+     (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p | 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: "[| sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+lemma S3S4S5S6LeadstoS6: "[| sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
          sigma |= S4 rmhist p & ires!p = #NotAResult
-                  ~> (S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p;
-         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
-         sigma |= S5 rmhist p ~> S6 rmhist p |]
-      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p ~> S6 rmhist p"
+                  \<leadsto> (S4 rmhist p & ires!p \<noteq> #NotAResult) | S5 rmhist p;
+         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
+      ==> sigma |= S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p \<leadsto> S6 rmhist p"
   apply (rule LatticeDisjunctionIntro [temp_use])
    apply (erule LatticeTriangle2 [temp_use])
    apply (rule S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
@@ -1157,14 +1157,14 @@
         intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
   done
 
-lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p ~> S3 rmhist p;
-         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+lemma S2S3S4S5S6LeadstoS6: "[| sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
+         sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
          sigma |= S4 rmhist p & ires!p = #NotAResult
-                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
-         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
-         sigma |= S5 rmhist p ~> S6 rmhist p |]
+                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
+         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
       ==> sigma |= S2 rmhist p | S3 rmhist p | S4 rmhist p | S5 rmhist p | S6 rmhist p
-                   ~> S6 rmhist p"
+                   \<leadsto> S6 rmhist p"
   apply (rule LatticeDisjunctionIntro [temp_use])
    apply (rule LatticeTransitivity [temp_use])
     prefer 2 apply assumption
@@ -1173,14 +1173,14 @@
          intro: ImplLeadsto_gen [temp_use] simp: Init_defs)
   done
 
-lemma NotS1LeadstoS6: "[| sigma |= []ImpInv rmhist p;
-         sigma |= S2 rmhist p ~> S3 rmhist p;
-         sigma |= S3 rmhist p ~> S4 rmhist p | S6 rmhist p;
+lemma NotS1LeadstoS6: "[| sigma |= \<box>ImpInv rmhist p;
+         sigma |= S2 rmhist p \<leadsto> S3 rmhist p;
+         sigma |= S3 rmhist p \<leadsto> S4 rmhist p | S6 rmhist p;
          sigma |= S4 rmhist p & ires!p = #NotAResult
-                  ~> S4 rmhist p & ires!p ~= #NotAResult | S5 rmhist p;
-         sigma |= S4 rmhist p & ires!p ~= #NotAResult ~> S5 rmhist p;
-         sigma |= S5 rmhist p ~> S6 rmhist p |]
-      ==> sigma |= ~S1 rmhist p ~> S6 rmhist p"
+                  \<leadsto> S4 rmhist p & ires!p \<noteq> #NotAResult | S5 rmhist p;
+         sigma |= S4 rmhist p & ires!p \<noteq> #NotAResult \<leadsto> S5 rmhist p;
+         sigma |= S5 rmhist p \<leadsto> S6 rmhist p |]
+      ==> sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p"
   apply (rule S2S3S4S5S6LeadstoS6 [THEN LatticeTransitivity [temp_use]])
        apply assumption+
   apply (erule INV_leadsto [temp_use])
@@ -1189,9 +1189,9 @@
   apply (auto simp: ImpInv_def Init_defs intro!: necT [temp_use])
   done
 
-lemma S1Infinite: "[| sigma |= ~S1 rmhist p ~> S6 rmhist p;
-         sigma |= []<>S6 rmhist p --> []<>S1 rmhist p |]
-      ==> sigma |= []<>S1 rmhist p"
+lemma S1Infinite: "[| sigma |= \<not>S1 rmhist p \<leadsto> S6 rmhist p;
+         sigma |= \<box>\<diamond>S6 rmhist p --> \<box>\<diamond>S1 rmhist p |]
+      ==> sigma |= \<box>\<diamond>S1 rmhist p"
   apply (rule classical)
   apply (tactic {* asm_lr_simp_tac (@{context} addsimps
     [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
@@ -1204,12 +1204,12 @@
    a. memory invariant
    b. "implementation invariant": always in states S1,...,S6
 *)
-lemma Step1_5_1a: "|- IPImp p --> (ALL l. []$MemInv mm l)"
+lemma Step1_5_1a: "|- IPImp p --> (\<forall>l. \<box>$MemInv mm l)"
   by (auto simp: IPImp_def box_stp_act [temp_use] intro!: MemoryInvariantAll [temp_use])
 
-lemma Step1_5_1b: "|- Init(ImpInit p & HInit rmhist p) & [](ImpNext p)
-         & [][HNext rmhist p]_(c p, r p, m p, rmhist!p) & [](ALL l. $MemInv mm l)
-         --> []ImpInv rmhist p"
+lemma Step1_5_1b: "|- 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)
+         --> \<box>ImpInv rmhist p"
   apply invariant
    apply (auto simp: Init_def ImpInv_def box_stp_act [temp_use]
      dest!: Step1_1 [temp_use] dest: S1_successors [temp_use] S2_successors [temp_use]
@@ -1222,9 +1222,9 @@
   by (auto simp: Init_def intro!: Step1_1 [temp_use] Step1_3  [temp_use])
 
 (*** step simulation ***)
-lemma Step1_5_2b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
-         & $ImpInv rmhist p & (!l. $MemInv mm l))
-         --> [][UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
+lemma Step1_5_2b: "|- \<box>(ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p)
+         & $ImpInv rmhist p & (\<forall>l. $MemInv mm l))
+         --> \<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])
@@ -1232,12 +1232,12 @@
 (*** Liveness ***)
 lemma GoodImpl: "|- IPImp p & HistP rmhist p
          -->   Init(ImpInit p & HInit rmhist p)
-             & [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-             & [](ALL l. $MemInv mm l) & []($ImpInv 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"
   apply clarsimp
-    apply (subgoal_tac "sigma |= Init (ImpInit p & HInit rmhist p) & [] (ImpNext p) &
-      [][HNext rmhist p]_ (c p, r p, m p, rmhist!p) & [] (ALL l. $MemInv mm l)")
+    apply (subgoal_tac "sigma |= 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 (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,10 +1251,10 @@
   done
 
 (* The implementation is infinitely often in state S1... *)
-lemma Step1_5_3a: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & [](ALL l. $MemInv mm l)
-         & []($ImpInv rmhist p) & ImpLive p
-         --> []<>S1 rmhist p"
+lemma Step1_5_3a: "|- \<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
+         --> \<box>\<diamond>S1 rmhist p"
   apply (clarsimp simp: ImpLive_def)
   apply (rule S1Infinite)
    apply (force simp: split_box_conj [try_rewrite] box_stp_act [try_rewrite]
@@ -1264,13 +1264,13 @@
   done
 
 (* ... and therefore satisfies the fairness requirements of the specification *)
-lemma Step1_5_3b: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3b: "|- \<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
          --> 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: "|- [](ImpNext p & [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & [](ALL l. $MemInv mm l) & []($ImpInv rmhist p) & ImpLive p
+lemma Step1_5_3c: "|- \<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
          --> WF(MemReturn memCh (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
   by (auto intro!: Return_fair [temp_use] Step1_5_3a [temp_use])
 
@@ -1296,25 +1296,25 @@
      apply (auto simp: square_def dest: S4Write [temp_use])
   done
 
-lemma Step2_2: "|-   (ALL p. ImpNext p)
-         & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-         & (ALL p. $ImpInv rmhist p)
-         & [EX q. Write rmCh mm ires q l]_(mm!l)
-         --> [EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
+lemma Step2_2: "|-   (\<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)
+         --> [\<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])+
     apply (force intro!: WriteS4 [temp_use])
    apply (auto dest!: Step2_2a [temp_use])
   done
 
-lemma Step2_lemma: "|- [](  (ALL p. ImpNext p)
-            & (ALL p. [HNext rmhist p]_(c p, r p, m p, rmhist!p))
-            & (ALL p. $ImpInv rmhist p)
-            & [EX q. Write rmCh mm ires q l]_(mm!l))
-         --> [][EX q. Write memCh mm (resbar rmhist) q l]_(mm!l)"
+lemma Step2_lemma: "|- \<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))
+         --> \<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: "|- #l : #MemLoc & (ALL p. IPImp p & HistP rmhist p)
+lemma Step2: "|- #l : #MemLoc & (\<forall>p. IPImp p & HistP rmhist p)
          --> MSpec memCh mm (resbar rmhist) l"
   apply (auto simp: MSpec_def)
    apply (force simp: IPImp_def MSpec_def)