--- a/src/HOL/TLA/Memory/MemClerkParameters.thy Fri Jun 26 11:44:22 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy Fri Jun 26 14:53:15 2015 +0200
@@ -17,12 +17,12 @@
definition
(* translate a memory call to an RPC call *)
- MClkRelayArg :: "memOp => rpcOp"
+ MClkRelayArg :: "memOp \<Rightarrow> rpcOp"
where "MClkRelayArg marg = memcall marg"
definition
(* translate RPC failures to memory failures *)
- MClkReplyVal :: "Vals => Vals"
+ MClkReplyVal :: "Vals \<Rightarrow> Vals"
where "MClkReplyVal v = (if v = RPCFailure then MemFailure else v)"
end