17 | Var "name" |
17 | Var "name" |
18 | App "rtrm" "rtrm" |
18 | App "rtrm" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
19 | Lam "rty" "name" "rtrm" |
20 |
20 |
21 |
21 |
22 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *} |
22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} |
23 print_theorems |
23 print_theorems |
24 |
24 |
25 local_setup {* |
25 local_setup {* |
26 snd o define_fv_alpha "LFex.rkind" |
26 snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") |
27 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
27 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
28 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
28 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
29 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
29 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
30 notation |
30 notation |
31 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
31 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |