| changeset 16417 | 9bc16273c2d4 |
| parent 11809 | c9ffdd63dd93 |
| child 18153 | a084aa91f701 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 |
1 |
2 header {* Nested datatypes *} |
2 header {* Nested datatypes *} |
3 |
3 |
4 theory NestedDatatype = Main: |
4 theory NestedDatatype imports Main begin |
5 |
5 |
6 subsection {* Terms and substitution *} |
6 subsection {* Terms and substitution *} |
7 |
7 |
8 datatype ('a, 'b) "term" = |
8 datatype ('a, 'b) "term" = |
9 Var 'a |
9 Var 'a |