diff -r f6335d319e9f -r db63752140c7 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Memory/RPC.thy	Mon Feb 08 13:02:56 1999 +0100
@@ -7,15 +7,13 @@
     Logic Image: TLA
 
     RPC-Memory example: RPC specification
-    For simplicity, specify the instance of RPC that is used in the
-    memory implementation (ignoring the BadCall exception).
 *)
 
-RPC = RPCParameters + ProcedureInterface +
+RPC = RPCParameters + ProcedureInterface + Memory +
 
 types
-  rpcSndChType  = "(rpcArgType,Vals) channel"
-  rpcRcvChType  = "(memArgType,Vals) channel"
+  rpcSndChType  = "(rpcOp,Vals) channel"
+  rpcRcvChType  = "memChType"
   rpcStType     = "(PrIds => rpcState) stfun"
 
 consts
@@ -34,49 +32,47 @@
   RPCISpec   :: "rpcSndChType => rpcRcvChType => rpcStType => temporal"
 
 rules
-  RPCInit_def       "$(RPCInit rcv rst p) .= 
-                         ($(rst@p) .= # rpcA
-                          .& .~ $(Calling rcv p))"
+  RPCInit_def       "RPCInit rcv rst p == PRED ((rst!p = #rpcA) & ~Calling rcv p)"
 
-  RPCFwd_def        "RPCFwd send rcv rst 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)"
+                         & $(rst!p) = # rpcA
+                         & IsLegalRcvArg<arg<$(send!p)>>
+                         & Call rcv p RPCRelayArg<arg<send!p>>
+                         & (rst!p)$ = # rpcB
+                         & unchanged (rtrner send!p)"
 
-  RPCReject_def     "RPCReject send rcv rst p ==
-                         $(rst@p) .= # rpcA
-                         .& .~ IsLegalRcvArg[ arg[ $(send@p) ] ]
-                         .& Return send p (#BadCall)
-                         .& unchanged <(rst@p), (caller rcv @ p)>"
+  RPCReject_def     "RPCReject send rcv rst p == ACT
+                           $(rst!p) = # rpcA
+                         & ~IsLegalRcvArg<arg<$(send!p)>>
+                         & Return send p #BadCall
+                         & unchanged ((rst!p), (caller rcv!p))"
 
-  RPCFail_def       "RPCFail send rcv rst p ==
-                         .~ $(Calling rcv p)
-                         .& Return send p (#RPCFailure)
-                         .& (rst@p)$ .= #rpcA
-                         .& unchanged (caller rcv @ p)"
+  RPCFail_def       "RPCFail send rcv rst p == ACT
+                           ~$(Calling rcv p)
+                         & Return send p #RPCFailure
+                         & (rst!p)$ = #rpcA
+                         & unchanged (caller rcv!p)"
 
-  RPCReply_def      "RPCReply send rcv rst p ==
-                         .~ $(Calling rcv p)
-                         .& $(rst@p) .= #rpcB
-                         .& Return send p (res[$(rcv@p)])
-                         .& (rst@p)$ .= #rpcA
-                         .& unchanged (caller rcv @ p)"
+  RPCReply_def      "RPCReply send rcv rst p == ACT
+                           ~$(Calling rcv p)
+                         & $(rst!p) = #rpcB
+		         & Return send p res<rcv!p>
+                         & (rst!p)$ = #rpcA
+                         & unchanged (caller rcv!p)"
 
-  RPCNext_def       "RPCNext send rcv rst p ==
-                         RPCFwd send rcv rst p
-                         .| RPCReject send rcv rst p
-                         .| RPCFail send rcv rst p
-                         .| RPCReply send rcv rst 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)"
 
-  RPCIPSpec_def     "RPCIPSpec send rcv rst p ==
-                         Init($(RPCInit rcv rst p))
-                         .& [][ 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>"
+  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)
+                         & WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
 
-  RPCISpec_def      "RPCISpec send rcv rst == RALL p. RPCIPSpec send rcv rst p"
+  RPCISpec_def      "RPCISpec send rcv rst == TEMP (! p. RPCIPSpec send rcv rst p)"
 
 end