src/HOL/TLA/Memory/MemClerk.thy

 (*
     File:        MemClerk.thy
+    ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1997 University of Munich
 
     Theory Name: MemClerk
     Logic Image: TLA
 
     RPC-Memory example: specification of the memory clerk.
 *)
 
-MemClerk = Memory + RPC + MemClerkParameters +
+theory MemClerk
+imports Memory RPC MemClerkParameters
+begin
 
 types
   (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
   mClkSndChType = "memChType"
   mClkRcvChType = "rpcSndChType"

                          & SF(MClkReply send rcv cst p)_(cst!p, rtrner send!p, caller rcv!p)"
 
   MClkISpec     :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
       "MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end