| changeset 1186 | 166cc41091b9 |
| parent 1185 | 7566b899ca6a |
| child 1187 | 3b24f33aedad |
| 1185:7566b899ca6a | 1186:166cc41091b9 |
|---|---|
430 rbv5 |
430 rbv5 |
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 |
|
436 (* |
|
435 local_setup {* define_raw_fv "Terms.rtrm5" [ |
437 local_setup {* define_raw_fv "Terms.rtrm5" [ |
436 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
438 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]] ] *} |
437 print_theorems |
439 print_theorems |
440 *) |
|
441 (* Alternate version with additional binding of name in rlts in rLcons *) |
|
442 local_setup {* define_raw_fv "Terms.rtrm5" [ |
|
443 [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]] ] *} |
|
444 print_theorems |
|
445 |
|
438 |
446 |
439 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
447 setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *} |
440 print_theorems |
448 print_theorems |
441 |
449 |
442 inductive |
450 inductive |