equal
deleted
inserted
replaced
33 | "bn2 (As x y t) = [atom y]" |
33 | "bn2 (As x y t) = [atom y]" |
34 | "bn3 (As x y t) = [atom x, atom y]" |
34 | "bn3 (As x y t) = [atom x, atom y]" |
35 | "bn4 (BNil) = {}" |
35 | "bn4 (BNil) = {}" |
36 | "bn4 (BAs a as) = {atom a} \<union> bn4 as" |
36 | "bn4 (BAs a as) = {atom a} \<union> bn4 as" |
37 |
37 |
|
38 thm foo.perm_bn_alpha |
|
39 thm foo.perm_bn_simps |
|
40 thm foo.bn_finite |
38 |
41 |
39 thm foo.distinct |
42 thm foo.distinct |
40 thm foo.induct |
43 thm foo.induct |
41 thm foo.inducts |
44 thm foo.inducts |
42 thm foo.exhaust |
45 thm foo.exhaust |