diff -r 8a4c44cef353 -r 16ffbc8442ca Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Thu Dec 23 01:05:05 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Sun Dec 26 16:35:16 2010 +0000 @@ -24,13 +24,15 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" + + + thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha thm foo.perm_bn_simps thm foo.bn_finite - thm foo.distinct thm foo.induct thm foo.inducts