diff -r b151399bd2c3 -r e1764a73c292 Nominal/Ex/SingleLet.thy --- 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