diff -r bcf558c445a4 -r 90779aefbf1a Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Wed Dec 08 13:16:25 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Wed Dec 08 17:07:08 2010 +0000 @@ -24,6 +24,10 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" +term "bn" + + + thm foo.bn_defs thm foo.permute_bn thm foo.perm_bn_alpha