equal
deleted
inserted
replaced
16 where |
16 where |
17 "rbv7 (rVr7 n) = {atom n}" |
17 "rbv7 (rVr7 n) = {atom n}" |
18 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
18 | "rbv7 (rLm7 n t) = rbv7 t - {atom n}" |
19 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
19 | "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r" |
20 |
20 |
21 setup {* snd o define_raw_perms ["rtrm7"] ["Term7.rtrm7"] *} |
21 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *} |
22 thm permute_rtrm7.simps |
22 thm permute_rtrm7.simps |
23 |
23 |
24 local_setup {* snd o define_fv_alpha "Term7.rtrm7" [ |
24 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [ |
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *} |
26 print_theorems |
26 print_theorems |
27 notation |
27 notation |
28 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
28 alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100) |
29 thm alpha_rtrm7.intros |
29 thm alpha_rtrm7.intros |