changeset 2132 | d74e08799b63 |
parent 2130 | 5111dadd1162 |
child 2133 | 16834a4ca1bb |
--- a/Nominal/Ex/SingleLetFoo.thy Fri May 14 10:21:14 2010 +0200 +++ b/Nominal/Ex/SingleLetFoo.thy Fri May 14 10:28:42 2010 +0200 @@ -3,8 +3,7 @@ begin -declare [[STEPS = 4]] -(* alpha does not work for this type *) +declare [[STEPS = 5]] atom_decl name @@ -22,6 +21,11 @@ where "bn (As x t) = {atom x}" +thm trm_assg.distinct +thm trm_assg.eq_iff +thm trm_assg.supp +thm trm_assg.perm + thm permute_trm_raw_permute_assg_raw.simps thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]