| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 58880 | 0baae4311a9f |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
6 |
6 |
7 theory Action |
7 theory Action |
8 imports Packet |
8 imports Packet |
9 begin |
9 begin |
10 |
10 |
11 datatype_new 'm action = S_msg 'm | R_msg 'm |
11 datatype 'm action = S_msg 'm | R_msg 'm |
12 | S_pkt "'m packet" | R_pkt "'m packet" |
12 | S_pkt "'m packet" | R_pkt "'m packet" |
13 | S_ack bool | R_ack bool |
13 | S_ack bool | R_ack bool |
14 | C_m_s | C_m_r | C_r_s | C_r_r 'm |
14 | C_m_s | C_m_r | C_r_s | C_r_r 'm |
15 |
15 |
16 end |
16 end |