| changeset 40774 | 0437dbc127b3 |
| parent 35174 | e15040ae75d7 |
| child 42151 | 4da4fc77664b |
| 40773:6c12f5e24e34 | 40774:0437dbc127b3 |
|---|---|
1 (* Title: HOL/IOA/NTP/Action.thy |
|
2 Author: Tobias Nipkow & Konrad Slind |
|
3 *) |
|
4 |
|
5 header {* The set of all actions of the system *} |
|
6 |
|
7 theory Action |
|
8 imports Packet |
|
9 begin |
|
10 |
|
11 datatype '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 |
|
16 end |