src/HOL/TLA/Memory/RPCMemoryParams.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 6255 db63752140c7
child 16417 9bc16273c2d4
permissions -rw-r--r--
tuned;
wenzelm@3807
     1
(* 
wenzelm@3807
     2
    File:        RPCMemoryParams.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: RPCMemoryParams
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    Basic declarations for the RPC-memory example.
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@11703
    12
theory RPCMemoryParams = Main:
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@6255
    15
  bit = "bool"   (* Signal wires for the procedure interface.
wenzelm@6255
    16
                    Defined as bool for simplicity. All I should really need is
wenzelm@6255
    17
                    the existence of two distinct values. *)
wenzelm@3807
    18
wenzelm@3807
    19
(* all of these are simple (HOL) types *)
wenzelm@11703
    20
typedecl Locs    (* "syntactic" value type *)
wenzelm@11703
    21
typedecl Vals    (* "syntactic" value type *)
wenzelm@11703
    22
typedecl PrIds   (* process id's *)
wenzelm@3807
    23
wenzelm@3807
    24
end