equal
deleted
inserted
replaced
14 rbv9 |
14 rbv9 |
15 where |
15 where |
16 "rbv9 (Var9 x) = {}" |
16 "rbv9 (Var9 x) = {}" |
17 | "rbv9 (Lam9 x b) = {atom x}" |
17 | "rbv9 (Lam9 x b) = {atom x}" |
18 |
18 |
19 setup {* snd o define_raw_perms ["rlam9", "rbla9"] ["Term9.rlam9", "Term9.rbla9"] *} |
19 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term9.rlam9") 2 *} |
20 print_theorems |
20 print_theorems |
21 |
21 |
22 local_setup {* snd o define_fv_alpha "Term9.rlam9" [ |
22 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term9.rlam9") [ |
23 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
23 [[[]], [[(NONE, 0)], [(NONE, 0)]]], [[[], [(SOME @{term rbv9}, 0)]]]] *} |
24 notation |
24 notation |
25 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
25 alpha_rlam9 ("_ \<approx>9l' _" [100, 100] 100) and |
26 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
26 alpha_rbla9 ("_ \<approx>9b' _" [100, 100] 100) |
27 thm alpha_rlam9_alpha_rbla9.intros |
27 thm alpha_rlam9_alpha_rbla9.intros |