| changeset 58249 | 180f1b3508ed |
| parent 42151 | 4da4fc77664b |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
6 |
6 |
7 theory TrivEx |
7 theory TrivEx |
8 imports Abstraction |
8 imports Abstraction |
9 begin |
9 begin |
10 |
10 |
11 datatype action = INC |
11 datatype_new 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 |