changeset 2886 | d7066575cbb9 |
parent 2885 | 1264f2a21ea9 |
child 2950 | 0911cb7bf696 |
--- a/Nominal/Ex/TypeSchemes.thy Wed Jun 22 12:18:22 2011 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 22 13:40:25 2011 +0100 @@ -4,15 +4,6 @@ section {*** Type Schemes ***} -datatype foo = - Foo1 -| Foo2 bar -and bar = - Bar - -ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *} - - atom_decl name (* defined as a single nominal datatype *)