--- a/Nominal/Ex/Foo1.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -35,6 +35,9 @@
 | "bn4 (BNil) = {}"
 | "bn4 (BAs a as) = {atom a} \<union> bn4 as"
 
+thm foo.perm_bn_alpha
+thm foo.perm_bn_simps
+thm foo.bn_finite
 
 thm foo.distinct
 thm foo.induct