--- a/src/HOL/TLA/Memory/MemClerk.thy Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
(*
File: MemClerk.thy
+ ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
@@ -9,7 +10,9 @@
RPC-Memory example: specification of the memory clerk.
*)
-MemClerk = Memory + RPC + MemClerkParameters +
+theory MemClerk
+imports Memory RPC MemClerkParameters
+begin
types
(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
@@ -64,4 +67,6 @@
MClkISpec :: "mClkSndChType => mClkRcvChType => mClkStType => temporal"
"MClkISpec send rcv cst == TEMP (ALL p. MClkIPSpec send rcv cst p)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end