--- 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