equal
deleted
inserted
replaced
16 where |
16 where |
17 "rbv6 (rVr6 n) = {}" |
17 "rbv6 (rVr6 n) = {}" |
18 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
18 | "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t" |
19 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
19 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r" |
20 |
20 |
21 setup {* snd o define_raw_perms ["rtrm6"] ["Term6.rtrm6"] *} |
21 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term6.rtrm6") 1 *} |
22 print_theorems |
22 print_theorems |
23 |
23 |
24 local_setup {* snd o define_fv_alpha "Term6.rtrm6" [ |
24 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term6.rtrm6") [ |
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
25 [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv6}, 0)]]]] *} |
26 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
26 notation alpha_rtrm6 ("_ \<approx>6 _" [100, 100] 100) |
27 thm alpha_rtrm6.intros |
27 thm alpha_rtrm6.intros |
28 |
28 |
29 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
29 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |