| changeset 1187 | 3b24f33aedad |
| parent 1186 | 166cc41091b9 |
| child 1190 | d900d19931fa |
| 1186:166cc41091b9 | 1187:3b24f33aedad |
|---|---|
431 where |
431 where |
432 "rbv5 rLnil = {}" |
432 "rbv5 rLnil = {}" |
433 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
433 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)" |
434 |
434 |
435 |
435 |
436 (* |
|
437 local_setup {* define_raw_fv "Terms.rtrm5" [ |
436 local_setup {* define_raw_fv "Terms.rtrm5" [ |
438 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
437 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
439 print_theorems |
438 print_theorems |
440 *) |
439 |
441 (* Alternate version with additional binding of name in rlts in rLcons *) |
440 (* Alternate version with additional binding of name in rlts in rLcons *) |
442 local_setup {* define_raw_fv "Terms.rtrm5" [ |
441 (*local_setup {* define_raw_fv "Terms.rtrm5" [ |
443 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
442 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
444 print_theorems |
443 print_theorems*) |
445 |
444 |
446 |
445 |
447 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
446 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
448 print_theorems |
447 print_theorems |
449 |
448 |