src/HOL/TLA/Memory/RPCMemoryParams.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 42018 878f33040280
child 60592 c9bd1d902f04
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      HOL/TLA/Memory/RPCMemoryParams.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 section {* 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