1(* Title: HOL/HOLCF/IOA/NTP/Action.thy 2 Author: Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>The set of all actions of the system\<close> 6 7theory Action 8imports Packet 9begin 10 11datatype 'm action = S_msg 'm | R_msg 'm 12 | S_pkt "'m packet" | R_pkt "'m packet" 13 | S_ack bool | R_ack bool 14 | C_m_s | C_m_r | C_r_s | C_r_r 'm 15 16end 17