22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "LFex.rkind") 3 *} |
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 (Datatype.the_info @{theory} "LFex.rkind") |
26 snd o define_fv_alpha (Datatype.the_info @{theory} "LFex.rkind") |
27 [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ], |
27 [[ [], [(NONE, 1, 2)]], |
28 [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ], |
28 [ [], [], [(NONE, 1, 2)] ], |
29 [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]] *} |
29 [ [], [], [], [(NONE, 1, 2)]]] *} |
30 notation |
30 notation |
31 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
31 alpha_rkind ("_ \<approx>ki _" [100, 100] 100) |
32 and alpha_rty ("_ \<approx>ty _" [100, 100] 100) |
32 and alpha_rty ("_ \<approx>ty _" [100, 100] 100) |
33 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
33 and alpha_rtrm ("_ \<approx>tr _" [100, 100] 100) |
34 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |
34 thm fv_rkind_fv_rty_fv_rtrm.simps alpha_rkind_alpha_rty_alpha_rtrm.intros |