--- a/src/HOL/TLA/Memory/MemoryParameters.thy Thu Aug 03 19:28:37 2000 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Thu Aug 03 19:29:03 2000 +0200
@@ -12,19 +12,8 @@
MemoryParameters = Datatype + RPCMemoryParams +
(* the memory operations *)
-(***
-datatype Rd = read
-datatype Wr = write
-***)
-
datatype memOp = read Locs | write Locs Vals
-(***
-types
- (* legal arguments for the memory *)
- memArgType = "(Rd * Locs) + (Wr * Locs * Vals)"
-***)
-
consts
(* memory locations and contents *)
MemLoc :: Locs set