src/HOL/TLA/Memory/MemClerkParameters.thy
changeset 17309 c43ed29bd197
parent 11703 6e5de8d4290a
child 21624 6f79647cf536
     1.1 --- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed Sep 07 20:22:15 2005 +0200
     1.2 +++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Wed Sep 07 20:22:39 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (*
     1.5      File:        MemClerkParameters.thy
     1.6 +    ID:          $Id$
     1.7      Author:      Stephan Merz
     1.8      Copyright:   1997 University of Munich
     1.9  
    1.10 @@ -9,9 +10,11 @@
    1.11      RPC-Memory example: Parameters of the memory clerk.
    1.12  *)
    1.13  
    1.14 -MemClerkParameters = RPCParameters + 
    1.15 +theory MemClerkParameters
    1.16 +imports RPCParameters
    1.17 +begin
    1.18  
    1.19 -datatype  mClkState  =  clkA | clkB
    1.20 +datatype mClkState = clkA | clkB
    1.21  
    1.22  types
    1.23    (* types sent on the clerk's send and receive channels are argument types
    1.24 @@ -27,4 +30,6 @@
    1.25    MClkReplyVal     :: "Vals => Vals"
    1.26      "MClkReplyVal v == if v = RPCFailure then MemFailure else v"
    1.27  
    1.28 +ML {* use_legacy_bindings (the_context ()) *}
    1.29 +
    1.30  end