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