equal
deleted
inserted
replaced
1 (* Title: HOL/IOA/NTP/Action.thy |
1 (* Title: HOL/IOA/NTP/Action.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow & Konrad Slind |
3 Author: Tobias Nipkow & Konrad Slind |
4 |
|
5 The set of all actions of the system. |
|
6 *) |
4 *) |
7 |
5 |
8 Action = Packet + Datatype + |
6 header {* The set of all actions of the system *} |
9 datatype 'm action = S_msg ('m) | R_msg ('m) |
7 |
10 | S_pkt ('m packet) | R_pkt ('m packet) |
8 theory Action |
11 | S_ack (bool) | R_ack (bool) |
9 imports Packet |
12 | C_m_s | C_m_r | C_r_s | C_r_r ('m) |
10 begin |
|
11 |
|
12 datatype 'm action = S_msg 'm | R_msg 'm |
|
13 | S_pkt "'m packet" | R_pkt "'m packet" |
|
14 | S_ack bool | R_ack bool |
|
15 | C_m_s | C_m_r | C_r_s | C_r_r 'm |
|
16 |
|
17 ML {* use_legacy_bindings (the_context ()) *} |
|
18 |
13 end |
19 end |