src/HOL/TLA/Memory/RPCParameters.thy
changeset 41589 bbd861837ebc
parent 32960 69916a850301
child 47968 3119ad2b5ad3
equal deleted inserted replaced
41588:9546828c0eb3 41589:bbd861837ebc
     1 (*
     1 (*  Title:      HOL/TLA/Memory/RPCParameters.thy
     2     File:        RPCParameters.thy
     2     Author:     Stephan Merz, University of Munich
     3     ID:          $Id$
       
     4     Author:      Stephan Merz
       
     5     Copyright:   1997 University of Munich
       
     6 *)
     3 *)
     7 
     4 
     8 header {* RPC-Memory example: RPC parameters *}
     5 header {* RPC-Memory example: RPC parameters *}
     9 
     6 
    10 theory RPCParameters
     7 theory RPCParameters