--- a/Nominal/Ex/Ex1.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Ex1.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -20,6 +20,11 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
+thm foo_bar.perm_bn_alpha
+thm foo_bar.perm_bn_simps
+thm foo_bar.bn_finite
+
+thm foo_bar.eq_iff
 thm foo_bar.distinct
 thm foo_bar.induct
 thm foo_bar.inducts