| changeset 41818 | 6d4c3ee8219d |
| parent 36862 | 952b2b102a0a |
| child 44174 | d1d79f0e1ea6 |
| 41817:c7be23634728 | 41818:6d4c3ee8219d |
|---|---|
8 header{*Mutual Induction via Iteratived Inductive Definitions*} |
8 header{*Mutual Induction via Iteratived Inductive Definitions*} |
9 |
9 |
10 theory Com imports Main begin |
10 theory Com imports Main begin |
11 |
11 |
12 typedecl loc |
12 typedecl loc |
13 types state = "loc => nat" |
13 type_synonym state = "loc => nat" |
14 |
14 |
15 datatype |
15 datatype |
16 exp = N nat |
16 exp = N nat |
17 | X loc |
17 | X loc |
18 | Op "nat => nat => nat" exp exp |
18 | Op "nat => nat => nat" exp exp |