changeset 41476 | 0fa9629aa399 |
parent 40945 | b8703f63bfb2 |
child 42151 | 4da4fc77664b |
41468:0e4f6cf20cdf | 41476:0fa9629aa399 |
---|---|
6 |
6 |
7 theory Receiver |
7 theory Receiver |
8 imports IOA Action Lemmas |
8 imports IOA Action Lemmas |
9 begin |
9 begin |
10 |
10 |
11 types |
11 type_synonym |
12 'm receiver_state = "'m list * bool" -- {* messages, mode *} |
12 'm receiver_state = "'m list * bool" -- {* messages, mode *} |
13 |
13 |
14 definition |
14 definition |
15 rq :: "'m receiver_state => 'm list" where |
15 rq :: "'m receiver_state => 'm list" where |
16 "rq = fst" |
16 "rq = fst" |