--- a/Nominal/Ex/Ex1.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/Ex1.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -18,8 +18,19 @@
   "bv (Bar0 x) = {}"
 | "bv (Bar1 v x b) = {atom v}"
 
-
-thm foo_bar.fv_defs[no_vars] foo_bar.bn_defs[no_vars]
+thm foo_bar.distinct
+thm foo_bar.induct
+thm foo_bar.inducts
+thm foo_bar.exhaust
+thm foo_bar.fv_defs
+thm foo_bar.bn_defs
+thm foo_bar.perm_simps
+thm foo_bar.eq_iff
+thm foo_bar.fv_bn_eqvt
+thm foo_bar.size_eqvt
+thm foo_bar.supports
+thm foo_bar.fsupp
+thm foo_bar.supp
 
 lemma
   "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}"