equal
deleted
inserted
replaced
4 |
4 |
5 S-expressions, general binary trees for defining recursive data |
5 S-expressions, general binary trees for defining recursive data |
6 structures by hand. |
6 structures by hand. |
7 *) |
7 *) |
8 |
8 |
9 theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin |
9 theory Sexp |
|
10 imports Main |
|
11 begin |
10 |
12 |
11 type_synonym 'a item = "'a Datatype.item" |
13 type_synonym 'a item = "'a Datatype.item" |
12 abbreviation "Leaf == Datatype.Leaf" |
14 abbreviation "Leaf == Datatype.Leaf" |
13 abbreviation "Numb == Datatype.Numb" |
15 abbreviation "Numb == Datatype.Numb" |
14 |
16 |