changeset 58310 | 91ea607a34d8 |
parent 58249 | 180f1b3508ed |
child 58889 | 5b7a9633cfa8 |
58309:a09ec6daaa19 | 58310:91ea607a34d8 |
---|---|
6 |
6 |
7 theory ABexp |
7 theory ABexp |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 datatype_new 'a aexp = |
11 datatype 'a aexp = |
12 IF "'a bexp" "'a aexp" "'a aexp" |
12 IF "'a bexp" "'a aexp" "'a aexp" |
13 | Sum "'a aexp" "'a aexp" |
13 | Sum "'a aexp" "'a aexp" |
14 | Diff "'a aexp" "'a aexp" |
14 | Diff "'a aexp" "'a aexp" |
15 | Var 'a |
15 | Var 'a |
16 | Num nat |
16 | Num nat |