src/HOL/TLA/Memory/ProcedureInterface.thy
changeset 26351 d5125a62f839
parent 21624 6f79647cf536
child 35068 544867142ea4
equal deleted inserted replaced
26350:a170a190c5d3 26351:d5125a62f839
     6 *)
     6 *)
     7 
     7 
     8 header {* Procedure interface for RPC-Memory components *}
     8 header {* Procedure interface for RPC-Memory components *}
     9 
     9 
    10 theory ProcedureInterface
    10 theory ProcedureInterface
    11 imports TLA RPCMemoryParams
    11 imports "../TLA" RPCMemoryParams
    12 begin
    12 begin
    13 
    13 
    14 typedecl
    14 typedecl
    15   (* type of channels with argument type 'a and return type 'r.
    15   (* type of channels with argument type 'a and return type 'r.
    16      we model a channel as an array of variables (of type chan)
    16      we model a channel as an array of variables (of type chan)