equal
deleted
inserted
replaced
22 bn::"assg \<Rightarrow> atom list" |
22 bn::"assg \<Rightarrow> atom list" |
23 where |
23 where |
24 "bn (As x y t a) = [atom x] @ bn a" |
24 "bn (As x y t a) = [atom x] @ bn a" |
25 | "bn (As_Nil) = []" |
25 | "bn (As_Nil) = []" |
26 |
26 |
27 term "bn" |
27 ML {* |
28 |
28 Variable.import; |
29 |
29 Variable.import true @{thms foo.exhaust} @{context} |
|
30 *} |
30 |
31 |
31 thm foo.bn_defs |
32 thm foo.bn_defs |
32 thm foo.permute_bn |
33 thm foo.permute_bn |
33 thm foo.perm_bn_alpha |
34 thm foo.perm_bn_alpha |
34 thm foo.perm_bn_simps |
35 thm foo.perm_bn_simps |
40 thm foo.inducts |
41 thm foo.inducts |
41 thm foo.exhaust |
42 thm foo.exhaust |
42 thm foo.fv_defs |
43 thm foo.fv_defs |
43 thm foo.bn_defs |
44 thm foo.bn_defs |
44 thm foo.perm_simps |
45 thm foo.perm_simps |
45 thm foo.eq_iff(5) |
46 thm foo.eq_iff |
46 thm foo.fv_bn_eqvt |
47 thm foo.fv_bn_eqvt |
47 thm foo.size_eqvt |
48 thm foo.size_eqvt |
48 thm foo.supports |
49 thm foo.supports |
49 thm foo.fsupp |
50 thm foo.fsupp |
50 thm foo.supp |
51 thm foo.supp |
51 thm foo.fresh |
52 thm foo.fresh |
52 |
53 |
53 |
54 |
54 |
55 |
|
56 text {* *} |
55 |
57 |
56 |
58 |
57 |
59 |
58 (* |
60 (* |
59 thm at_set_avoiding1[THEN exE] |
61 thm at_set_avoiding1[THEN exE] |