changeset 2322 | 24de7e548094 |
parent 2320 | d835a2771608 |
child 2330 | 8728f7990f6d |
--- a/Nominal/Ex/SingleLet.thy Tue Jun 22 13:31:42 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Tue Jun 22 18:07:53 2010 +0100 @@ -4,7 +4,7 @@ atom_decl name -declare [[STEPS = 13]] +declare [[STEPS = 14]] nominal_datatype trm = Var "name" @@ -21,7 +21,6 @@ where "bn (As x y t) = {atom x}" - thm trm_assg.fv thm trm_assg.supp thm trm_assg.eq_iff