src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 6255 db63752140c7
parent 3807 82a99b090d9d
child 11703 6e5de8d4290a
     1.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Mon Feb 08 13:02:42 1999 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Mon Feb 08 13:02:56 1999 +0100
     1.3 @@ -16,19 +16,16 @@
     1.4  types
     1.5    (* types sent on the clerk's send and receive channels are argument types
     1.6       of the memory and the RPC, respectively *)
     1.7 -  mClkSndArgType   = "memArgType"
     1.8 -  mClkRcvArgType   = "rpcArgType"
     1.9 +  mClkSndArgType   = "memOp"
    1.10 +  mClkRcvArgType   = "rpcOp"
    1.11  
    1.12 -consts
    1.13 +constdefs
    1.14    (* translate a memory call to an RPC call *)
    1.15 -  MClkRelayArg     :: "memArgType => rpcArgType"
    1.16 +  MClkRelayArg     :: "memOp => rpcOp"
    1.17 +    "MClkRelayArg marg == memcall marg"
    1.18    (* translate RPC failures to memory failures *)
    1.19    MClkReplyVal     :: "Vals => Vals"
    1.20 -
    1.21 -rules
    1.22 -  MClkRelayArg_def    "MClkRelayArg marg == Inl (remoteCall, marg)"
    1.23 -  MClkReplyVal_def    "MClkReplyVal v == 
    1.24 -                           if v = RPCFailure then MemFailure else v"
    1.25 +    "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    1.26  
    1.27  end
    1.28