src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 36866 426d5781bb25
parent 21624 6f79647cf536
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed May 12 15:25:58 2010 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed May 12 16:44:49 2010 +0200
     1.3 @@ -19,12 +19,14 @@
     1.4    mClkSndArgType   = "memOp"
     1.5    mClkRcvArgType   = "rpcOp"
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    (* translate a memory call to an RPC call *)
    1.10    MClkRelayArg     :: "memOp => rpcOp"
    1.11 -    "MClkRelayArg marg == memcall marg"
    1.12 +  where "MClkRelayArg marg = memcall marg"
    1.13 +
    1.14 +definition
    1.15    (* translate RPC failures to memory failures *)
    1.16    MClkReplyVal     :: "Vals => Vals"
    1.17 -    "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    1.18 +  where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
    1.19  
    1.20  end