src/HOL/TLA/Memory/RPCMemoryParams.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 11703 6e5de8d4290a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:        RPCMemoryParams.thy
     3     Author:      Stephan Merz
     4     Copyright:   1997 University of Munich
     5 
     6     Theory Name: RPCMemoryParams
     7     Logic Image: TLA
     8 
     9     Basic declarations for the RPC-memory example.
    10 *)
    11 
    12 RPCMemoryParams = HOL +
    13 
    14 types
    15   bit = "bool"   (* Signal wires for the procedure interface.
    16                     Defined as bool for simplicity. All I should really need is
    17                     the existence of two distinct values. *)
    18   Locs           (* "syntactic" value type *)
    19   Vals           (* "syntactic" value type *)
    20   PrIds          (* process id's *)
    21 
    22 (* all of these are simple (HOL) types *)
    23 arities
    24   Locs   :: term
    25   Vals   :: term
    26   PrIds  :: term
    27 
    28 end