changeset 2556 | 8ed62410236e |
parent 2485 | 6bab47906dbe |
child 2557 | 781fbc8c0591 |
--- a/Nominal/Ex/Datatypes.thy Fri Nov 05 15:21:10 2010 +0000 +++ b/Nominal/Ex/Datatypes.thy Sat Nov 06 06:18:41 2010 +0000 @@ -7,6 +7,7 @@ atom_decl - example by John Matthews *) +(* FIXME: throws an problem with fv-function nominal_datatype 'a Maybe = Nothing | Just 'a @@ -22,6 +23,7 @@ thm Maybe.fv_bn_eqvt thm Maybe.size_eqvt thm Maybe.supp +*) (* using a datatype inside a nominal_datatype