| changeset 41818 | 6d4c3ee8219d |
| parent 32960 | 69916a850301 |
| child 44013 | 5cfc1c36ae97 |
| 41817:c7be23634728 | 41818:6d4c3ee8219d |
|---|---|
6 structures by hand. |
6 structures by hand. |
7 *) |
7 *) |
8 |
8 |
9 theory Sexp imports Main begin |
9 theory Sexp imports Main begin |
10 |
10 |
11 types |
11 type_synonym 'a item = "'a Datatype.item" |
12 'a item = "'a Datatype.item" |
|
13 abbreviation "Leaf == Datatype.Leaf" |
12 abbreviation "Leaf == Datatype.Leaf" |
14 abbreviation "Numb == Datatype.Numb" |
13 abbreviation "Numb == Datatype.Numb" |
15 |
14 |
16 inductive_set |
15 inductive_set |
17 sexp :: "'a item set" |
16 sexp :: "'a item set" |