diff -r 1d31e3a50373 -r 0318b43ee95c src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 11:07:04 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 11:44:22 2015 +0200
@@ -28,7 +28,7 @@
   RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
 
 defs
-  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
+  RPCInit_def:       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & \<not>Calling rcv p)"
 
   RPCFwd_def:        "RPCFwd send rcv rst p == ACT
                          $(Calling send p)
@@ -40,18 +40,18 @@
 
   RPCReject_def:     "RPCReject send rcv rst p == ACT
                            $(rst!p) = # rpcA
-                         & ~IsLegalRcvArg<arg<$(send!p)>>
+                         & \<not>IsLegalRcvArg<arg<$(send!p)>>
                          & Return send p #BadCall
                          & unchanged ((rst!p), (caller rcv!p))"
 
   RPCFail_def:       "RPCFail send rcv rst p == ACT
-                           ~$(Calling rcv p)
+                           \<not>$(Calling rcv p)
                          & Return send p #RPCFailure
                          & (rst!p)$ = #rpcA
                          & unchanged (caller rcv!p)"
 
   RPCReply_def:      "RPCReply send rcv rst p == ACT
-                           ~$(Calling rcv p)
+                           \<not>$(Calling rcv p)
                          & $(rst!p) = #rpcB
                          & Return send p res<rcv!p>
                          & (rst!p)$ = #rpcA
@@ -65,10 +65,10 @@
 
   RPCIPSpec_def:     "RPCIPSpec send rcv rst p == TEMP
                            Init RPCInit rcv rst p
-                         & [][ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!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)"
 
-  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (ALL p. RPCIPSpec send rcv rst p)"
+  RPCISpec_def:      "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
 
 
 lemmas RPC_action_defs =
@@ -81,10 +81,10 @@
    unanswered call for that process.
 *)
 
-lemma RPCidle: "|- ~$(Calling send p) --> ~RPCNext send rcv rst p"
+lemma RPCidle: "|- \<not>$(Calling send p) --> \<not>RPCNext send rcv rst p"
   by (auto simp: Return_def RPC_action_defs)
 
-lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> ~RPCNext send rcv rst p"
+lemma RPCbusy: "|- $(Calling rcv p) & $(rst!p) = #rpcB --> \<not>RPCNext send rcv rst p"
   by (auto simp: RPC_action_defs)
 
 (* RPC failure actions are visible. *)
@@ -97,14 +97,14 @@
   by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
 
 (* Enabledness of some actions *)
-lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
-    |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
+lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
+    |- \<not>Calling rcv p & Calling send p --> 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: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
-      |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
+lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
+      |- \<not>Calling rcv p & Calling send p & rst!p = #rpcB  
          --> 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]