--- a/Nominal/Ex/Modules.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Modules.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -63,6 +63,10 @@
 | "Cbinders (SVal v T) = {atom v}"
 
 
+thm modules.perm_bn_alpha
+thm modules.perm_bn_simps
+thm modules.bn_finite
+
 thm modules.distinct
 thm modules.induct
 thm modules.exhaust