equal
deleted
inserted
replaced
21 "rbv2 (rAs x t) = {atom x}" |
21 "rbv2 (rAs x t) = {atom x}" |
22 |
22 |
23 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} |
23 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} |
24 |
24 |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term2.rtrm2") |
26 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
26 [[[], |
27 [[[], []]]] *} |
27 [], |
|
28 [(NONE, 0, 1)], |
|
29 [(SOME @{term rbv2}, 0, 1)]], |
|
30 [[]]] *} |
28 |
31 |
29 notation |
32 notation |
30 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
33 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
31 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
34 alpha_rassign ("_ \<approx>2b _" [100, 100] 100) |
32 thm alpha_rtrm2_alpha_rassign.intros |
35 thm alpha_rtrm2_alpha_rassign.intros |