(* Title: HOL/IOA/example/Action.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
The set of all actions of the system
*)
Action = Packet +
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