| changeset 16417 | 9bc16273c2d4 |
| parent 13079 | e7738aa7267f |
| child 18413 | 50c0c118e96d |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
5 |
5 |
6 S-expressions, general binary trees for defining recursive data |
6 S-expressions, general binary trees for defining recursive data |
7 structures by hand. |
7 structures by hand. |
8 *) |
8 *) |
9 |
9 |
10 theory Sexp = Datatype_Universe + Inductive: |
10 theory Sexp imports Datatype_Universe Inductive begin |
11 consts |
11 consts |
12 sexp :: "'a item set" |
12 sexp :: "'a item set" |
13 |
13 |
14 inductive sexp |
14 inductive sexp |
15 intros |
15 intros |