src/HOL/TLA/Memory/RPCMemoryParams.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,28 @@
+(* 
+    File:        RPCMemoryParams.thy
+    Author:      Stephan Merz
+    Copyright:   1997 University of Munich
+
+    Theory Name: RPCMemoryParams
+    Logic Image: TLA
+
+    Basic declarations for the RPC-memory example.
+*)
+
+RPCMemoryParams = HOL +
+
+types
+  bit = "bool"   (* signal wires for the procedure interface *)
+                 (* Defined as bool for simplicity. All I should really need is *)
+                 (* the existence of two distinct values. *)
+  Locs           (* "syntactic" value type *)
+  Vals           (* "syntactic" value type *)
+  PrIds          (* process id's *)
+
+(* all of these are simple (HOL) types *)
+arities
+  Locs   :: term
+  Vals   :: term
+  PrIds  :: term
+
+end