| changeset 58249 | 180f1b3508ed |
| parent 42151 | 4da4fc77664b |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
6 |
6 |
7 theory Action |
7 theory Action |
8 imports Packet |
8 imports Packet |
9 begin |
9 begin |
10 |
10 |
11 datatype 'm action = |
11 datatype_new 'm action = |
12 Next | S_msg 'm | R_msg 'm |
12 Next | S_msg 'm | R_msg 'm |
13 | S_pkt "'m packet" | R_pkt "'m packet" |
13 | S_pkt "'m packet" | R_pkt "'m packet" |
14 | S_ack bool | R_ack bool |
14 | S_ack bool | R_ack bool |
15 |
15 |
16 end |
16 end |