diff -r ebf253d80670 -r 0f24c961b5f6 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri Jul 30 00:40:32 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Sat Jul 31 01:24:39 2010 +0100 @@ -21,6 +21,8 @@ where "bn (As x y t) = {atom x}" +thm alpha_sym_thms +thm alpha_trans_thms thm size_eqvt thm alpha_bn_imps thm distinct