| changeset 58310 | 91ea607a34d8 |
| parent 58249 | 180f1b3508ed |
| child 58880 | 0baae4311a9f |
| 58309:a09ec6daaa19 | 58310:91ea607a34d8 |
|---|---|
6 |
6 |
7 theory Abschannel |
7 theory Abschannel |
8 imports IOA Action |
8 imports IOA Action |
9 begin |
9 begin |
10 |
10 |
11 datatype_new 'a abs_action = S 'a | R 'a |
11 datatype 'a abs_action = S 'a | R 'a |
12 |
12 |
13 definition |
13 definition |
14 ch_asig :: "'a abs_action signature" where |
14 ch_asig :: "'a abs_action signature" where |
15 "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" |
15 "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})" |
16 |
16 |