Nominal/Ex/Foo2.thy
changeset 2628 16ffbc8442ca
parent 2626 d1bdc281be2b
child 2629 ffb5a181844b
--- 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