| changeset 16417 | 9bc16273c2d4 |
| parent 13535 | 007559e981c7 |
| child 18415 | eb68dc98bda2 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Trees and forests, a mutually recursive type definition *} |
7 header {* Trees and forests, a mutually recursive type definition *} |
8 |
8 |
9 theory Tree_Forest = Main: |
9 theory Tree_Forest imports Main begin |
10 |
10 |
11 subsection {* Datatype definition *} |
11 subsection {* Datatype definition *} |
12 |
12 |
13 consts |
13 consts |
14 tree :: "i => i" |
14 tree :: "i => i" |