src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 58249 180f1b3508ed
     1.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -10,11 +10,10 @@
     1.4  
     1.5  datatype mClkState = clkA | clkB
     1.6  
     1.7 -types
     1.8 -  (* types sent on the clerk's send and receive channels are argument types
     1.9 -     of the memory and the RPC, respectively *)
    1.10 -  mClkSndArgType   = "memOp"
    1.11 -  mClkRcvArgType   = "rpcOp"
    1.12 +(* types sent on the clerk's send and receive channels are argument types
    1.13 +   of the memory and the RPC, respectively *)
    1.14 +type_synonym mClkSndArgType = "memOp"
    1.15 +type_synonym mClkRcvArgType = "rpcOp"
    1.16  
    1.17  definition
    1.18    (* translate a memory call to an RPC call *)