changeset 58310 | 91ea607a34d8 |
parent 58249 | 180f1b3508ed |
child 58880 | 0baae4311a9f |
58309:a09ec6daaa19 | 58310:91ea607a34d8 |
---|---|
6 |
6 |
7 theory TrivEx |
7 theory TrivEx |
8 imports Abstraction |
8 imports Abstraction |
9 begin |
9 begin |
10 |
10 |
11 datatype_new action = INC |
11 datatype action = INC |
12 |
12 |
13 definition |
13 definition |
14 C_asig :: "action signature" where |
14 C_asig :: "action signature" where |
15 "C_asig = ({},{INC},{})" |
15 "C_asig = ({},{INC},{})" |
16 definition |
16 definition |