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