| changeset 1277 | 6eacf60ce41d |
| parent 1270 | 8c3cf9f4f5f2 |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
20 bv3 |
20 bv3 |
21 where |
21 where |
22 "bv3 rANil = {}" |
22 "bv3 rANil = {}" |
23 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)" |
23 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)" |
24 |
24 |
25 setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *} |
25 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *} |
26 |
26 |
27 local_setup {* snd o define_fv_alpha "Term3.rtrm3" |
27 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3") |
28 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
28 [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]], |
29 [[], [[], [], []]]] *} |
29 [[], [[], [], []]]] *} |
30 print_theorems |
30 print_theorems |
31 |
31 |
32 notation |
32 notation |