author | berghofe |
Mon, 05 Aug 2002 14:35:33 +0200 | |
changeset 13455 | f88a91ff8ac6 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
(* Title: HOLCF/IOA/ABP/Action.thy ID: $Id$ Author: Olaf Müller License: GPL (GNU GENERAL PUBLIC LICENSE) The set of all actions of the system. *) Action = Packet + Datatype + datatype 'm action = Next | S_msg ('m) | R_msg ('m) | S_pkt ('m packet) | R_pkt ('m packet) | S_ack (bool) | R_ack (bool) end