| changeset 58249 | 180f1b3508ed |
| parent 51717 | 9e7d1c139569 |
| child 58310 | 91ea607a34d8 |
| 58248:25af24e1f37b | 58249:180f1b3508ed |
|---|---|
7 theory Inc |
7 theory Inc |
8 imports TLA |
8 imports TLA |
9 begin |
9 begin |
10 |
10 |
11 (* program counter as an enumeration type *) |
11 (* program counter as an enumeration type *) |
12 datatype pcount = a | b | g |
12 datatype_new pcount = a | b | g |
13 |
13 |
14 axiomatization |
14 axiomatization |
15 (* program variables *) |
15 (* program variables *) |
16 x :: "nat stfun" and |
16 x :: "nat stfun" and |
17 y :: "nat stfun" and |
17 y :: "nat stfun" and |