equal
deleted
inserted
replaced
131 |
131 |
132 ML {* |
132 ML {* |
133 val thms_e = map (lift_thm qtys @{context}) |
133 val thms_e = map (lift_thm qtys @{context}) |
134 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
134 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
135 prod.cases]} |
135 prod.cases]} |
|
136 *} |
|
137 |
|
138 ML {* |
|
139 val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs} |
136 *} |
140 *} |
137 |
141 |
138 |
142 |
139 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
143 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
140 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
144 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |