| changeset 1277 | 6eacf60ce41d |
| parent 1270 | 8c3cf9f4f5f2 |
| 1276:3365fce80f0f | 1277:6eacf60ce41d |
|---|---|
15 rbv8 |
15 rbv8 |
16 where |
16 where |
17 "rbv8 (Bar0 x) = {}" |
17 "rbv8 (Bar0 x) = {}" |
18 | "rbv8 (Bar1 v x b) = {atom v}" |
18 | "rbv8 (Bar1 v x b) = {atom v}" |
19 |
19 |
20 setup {* snd o define_raw_perms ["rfoo8", "rbar8"] ["Term8.rfoo8", "Term8.rbar8"] *} |
20 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} |
21 print_theorems |
21 print_theorems |
22 |
22 |
23 local_setup {* snd o define_fv_alpha "Term8.rfoo8" [ |
23 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ |
24 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
24 [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
25 notation |
25 notation |
26 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
26 alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and |
27 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
27 alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100) |
28 thm alpha_rfoo8_alpha_rbar8.intros |
28 thm alpha_rfoo8_alpha_rbar8.intros |