--- 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