equal
deleted
inserted
replaced
8 |
8 |
9 theory Sexp |
9 theory Sexp |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
13 type_synonym 'a item = "'a Datatype.item" |
13 type_synonym 'a item = "'a Old_Datatype.item" |
14 abbreviation "Leaf == Datatype.Leaf" |
14 abbreviation "Leaf == Old_Datatype.Leaf" |
15 abbreviation "Numb == Datatype.Numb" |
15 abbreviation "Numb == Old_Datatype.Numb" |
16 |
16 |
17 inductive_set |
17 inductive_set |
18 sexp :: "'a item set" |
18 sexp :: "'a item set" |
19 where |
19 where |
20 LeafI: "Leaf(a) \<in> sexp" |
20 LeafI: "Leaf(a) \<in> sexp" |