| changeset 2886 | d7066575cbb9 |
| parent 2885 | 1264f2a21ea9 |
| child 2950 | 0911cb7bf696 |
| 2885:1264f2a21ea9 | 2886:d7066575cbb9 |
|---|---|
1 theory TypeSchemes |
1 theory TypeSchemes |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 section {*** Type Schemes ***} |
5 section {*** Type Schemes ***} |
6 |
|
7 datatype foo = |
|
8 Foo1 |
|
9 | Foo2 bar |
|
10 and bar = |
|
11 Bar |
|
12 |
|
13 ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *} |
|
14 |
|
15 |
6 |
16 atom_decl name |
7 atom_decl name |
17 |
8 |
18 (* defined as a single nominal datatype *) |
9 (* defined as a single nominal datatype *) |
19 |
10 |