equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>The implementation: receiver\<close> |
5 section \<open>The implementation: receiver\<close> |
6 |
6 |
7 theory Receiver |
7 theory Receiver |
8 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas |
8 imports "~~/src/HOL/HOLCF/IOA/IOA" Action Lemmas |
9 begin |
9 begin |
10 |
10 |
11 type_synonym |
11 type_synonym |
12 'm receiver_state = "'m list * bool" \<comment> \<open>messages, mode\<close> |
12 'm receiver_state = "'m list * bool" \<comment> \<open>messages, mode\<close> |
13 |
13 |