| changeset 1277 | 6eacf60ce41d |
| parent 1270 | 8c3cf9f4f5f2 |
| child 1278 | 8814494fe4da |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
18 primrec |
18 primrec |
19 rbv2 |
19 rbv2 |
20 where |
20 where |
21 "rbv2 (rAs x t) = {atom x}" |
21 "rbv2 (rAs x t) = {atom x}" |
22 |
22 |
23 setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Term2.rtrm2", "Term2.rassign"] *} |
23 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *} |
24 |
24 |
25 local_setup {* snd o define_fv_alpha "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 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]], |
27 [[[], []]]] *} |
27 [[[], []]]] *} |
28 |
28 |
29 notation |
29 notation |
30 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |
30 alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and |