src/HOL/TLA/Memory/MemClerk.thy
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 22:48:08 2011 +0100
     1.2 +++ b/src/HOL/TLA/Memory/MemClerk.thy	Sun Mar 20 23:07:06 2011 +0100
     1.3 @@ -8,11 +8,10 @@
     1.4  imports Memory RPC MemClerkParameters
     1.5  begin
     1.6  
     1.7 -types
     1.8 -  (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
     1.9 -  mClkSndChType = "memChType"
    1.10 -  mClkRcvChType = "rpcSndChType"
    1.11 -  mClkStType    = "(PrIds => mClkState) stfun"
    1.12 +(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
    1.13 +type_synonym mClkSndChType = "memChType"
    1.14 +type_synonym mClkRcvChType = "rpcSndChType"
    1.15 +type_synonym mClkStType = "(PrIds => mClkState) stfun"
    1.16  
    1.17  definition
    1.18    (* state predicates *)