equal
deleted
inserted
replaced
42 IsLegalRcvArg_def: "IsLegalRcvArg ra == |
42 IsLegalRcvArg_def: "IsLegalRcvArg ra == |
43 case ra of (memcall m) => True |
43 case ra of (memcall m) => True |
44 | (othercall v) => False" |
44 | (othercall v) => False" |
45 RPCRelayArg_def: "RPCRelayArg ra == |
45 RPCRelayArg_def: "RPCRelayArg ra == |
46 case ra of (memcall m) => m |
46 case ra of (memcall m) => m |
47 | (othercall v) => arbitrary" |
47 | (othercall v) => undefined" |
48 |
48 |
49 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF |
49 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF |
50 NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric] |
50 NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric] |
51 |
51 |
52 end |
52 end |