--- a/src/HOL/TLA/Memory/MemoryParameters.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemoryParameters.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,32 +10,37 @@
RPC-Memory example: Memory parameters
*)
-MemoryParameters = Datatype + RPCMemoryParams +
+theory MemoryParameters
+imports RPCMemoryParams
+begin
(* the memory operations *)
datatype memOp = read Locs | write Locs Vals
consts
(* memory locations and contents *)
- MemLoc :: Locs set
- MemVal :: Vals set
+ MemLoc :: "Locs set"
+ MemVal :: "Vals set"
(* some particular values *)
OK :: "Vals"
BadArg :: "Vals"
MemFailure :: "Vals"
NotAResult :: "Vals" (* defined here for simplicity *)
-
+
(* the initial value stored in each memory cell *)
InitVal :: "Vals"
-rules
+axioms
(* basic assumptions about the above constants and predicates *)
- BadArgNoMemVal "BadArg ~: MemVal"
- MemFailNoMemVal "MemFailure ~: MemVal"
- InitValMemVal "InitVal : MemVal"
- NotAResultNotVal "NotAResult ~: MemVal"
- NotAResultNotOK "NotAResult ~= OK"
- NotAResultNotBA "NotAResult ~= BadArg"
- NotAResultNotMF "NotAResult ~= MemFailure"
+ BadArgNoMemVal: "BadArg ~: MemVal"
+ MemFailNoMemVal: "MemFailure ~: MemVal"
+ InitValMemVal: "InitVal : MemVal"
+ NotAResultNotVal: "NotAResult ~: MemVal"
+ NotAResultNotOK: "NotAResult ~= OK"
+ NotAResultNotBA: "NotAResult ~= BadArg"
+ NotAResultNotMF: "NotAResult ~= MemFailure"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end