| changeset 1277 | 6eacf60ce41d |
| parent 1270 | 8c3cf9f4f5f2 |
| child 1286 | 87894b5156f4 |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
17 where |
17 where |
18 "rbv5 rLnil = {}" |
18 "rbv5 rLnil = {}" |
19 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
19 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
20 |
20 |
21 |
21 |
22 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Term5.rtrm5", "Term5.rlts"] *} |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *} |
23 print_theorems |
23 print_theorems |
24 |
24 |
25 local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5") [ |
26 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
26 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
27 print_theorems |
27 print_theorems |
28 |
28 |
29 (* Alternate version with additional binding of name in rlts in rLcons *) |
29 (* Alternate version with additional binding of name in rlts in rLcons *) |
30 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |
30 (*local_setup {* snd o define_fv_alpha "Term5.rtrm5" [ |