src/HOL/HOLCF/IOA/NTP/Action.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 58310 91ea607a34d8
child 62002 f1599e98c4d0
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/IOA/NTP/Action.thy
mueller@3073
     2
    Author:     Tobias Nipkow & Konrad Slind
mueller@3073
     3
*)
mueller@3073
     4
wenzelm@58880
     5
section {* The set of all actions of the system *}
wenzelm@17244
     6
wenzelm@17244
     7
theory Action
wenzelm@17244
     8
imports Packet
wenzelm@17244
     9
begin
wenzelm@17244
    10
blanchet@58310
    11
datatype 'm action = S_msg 'm | R_msg 'm
wenzelm@17244
    12
                   | S_pkt "'m packet" | R_pkt "'m packet"
wenzelm@17244
    13
                   | S_ack bool | R_ack bool
wenzelm@17244
    14
                   | C_m_s | C_m_r | C_r_s | C_r_r 'm
wenzelm@17244
    15
mueller@3073
    16
end