src/HOL/TLA/Memory/RPCMemoryParams.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 58889 5b7a9633cfa8
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/RPCMemoryParams.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* Basic declarations for the RPC-memory example *}
     6 
     7 theory RPCMemoryParams
     8 imports Main
     9 begin
    10 
    11 type_synonym bit = "bool"
    12  (* Signal wires for the procedure interface.
    13     Defined as bool for simplicity. All I should really need is
    14     the existence of two distinct values. *)
    15 
    16 (* all of these are simple (HOL) types *)
    17 typedecl Locs    (* "syntactic" value type *)
    18 typedecl Vals    (* "syntactic" value type *)
    19 typedecl PrIds   (* process id's *)
    20 
    21 end