equal
deleted
inserted
replaced
136 *} |
136 *} |
137 |
137 |
138 ML {* |
138 ML {* |
139 val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs} |
139 val thms_f = map (lift_thm qtys @{context}) @{thms bn_defs} |
140 *} |
140 *} |
|
141 |
|
142 ML {* |
|
143 val thms_f = map (lift_thm qtys @{context}) @{thms bn_eqvt} |
|
144 *} |
|
145 |
|
146 ML {* |
|
147 val thms_f = map (lift_thm qtys @{context}) @{thms fv_eqvt} |
|
148 *} |
|
149 |
|
150 ML {* |
|
151 val thms_f = map (lift_thm qtys @{context}) @{thms size_eqvt} |
|
152 *} |
|
153 |
|
154 |
141 |
155 |
142 |
156 |
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) |
157 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) |
144 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
158 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] |
145 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |
159 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm |