--- a/src/HOL/TLA/Memory/MemClerk.thy Sun Mar 20 22:48:08 2011 +0100
+++ b/src/HOL/TLA/Memory/MemClerk.thy Sun Mar 20 23:07:06 2011 +0100
@@ -8,11 +8,10 @@
imports Memory RPC MemClerkParameters
begin
-types
- (* The clerk takes the same arguments as the memory and sends requests to the RPC *)
- mClkSndChType = "memChType"
- mClkRcvChType = "rpcSndChType"
- mClkStType = "(PrIds => mClkState) stfun"
+(* The clerk takes the same arguments as the memory and sends requests to the RPC *)
+type_synonym mClkSndChType = "memChType"
+type_synonym mClkRcvChType = "rpcSndChType"
+type_synonym mClkStType = "(PrIds => mClkState) stfun"
definition
(* state predicates *)