changeset 2338 | e1764a73c292 |
parent 2336 | f2d545b77b31 |
child 2339 | 1e0b3992189c |
--- a/Nominal/Ex/SingleLet.thy Sun Jun 27 21:41:21 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Mon Jun 28 15:23:56 2010 +0100 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 15]] +declare [[STEPS = 16]] nominal_datatype trm = Var "name" @@ -21,6 +21,11 @@ where "bn (As x y t) = {atom x}" +term Var +term App +term Baz + + typ trm typ assg