297 |
297 |
298 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar |
298 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar |
299 co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
299 co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
300 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...}, |
300 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...}, |
301 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
301 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
302 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
302 rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, |
|
303 set_cases, ...}, |
303 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
304 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
304 co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, |
305 co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, |
305 set_inducts, ...}, |
306 set_inducts, ...}, |
306 ...} : fp_sugar) = |
307 ...} : fp_sugar) = |
307 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
308 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
323 rel_injects = rel_injects, |
324 rel_injects = rel_injects, |
324 rel_distincts = rel_distincts, |
325 rel_distincts = rel_distincts, |
325 rel_sels = rel_sels, |
326 rel_sels = rel_sels, |
326 rel_intros = rel_intros, |
327 rel_intros = rel_intros, |
327 rel_cases = rel_cases, |
328 rel_cases = rel_cases, |
|
329 pred_injects = pred_injects, |
328 set_thms = set_thms, |
330 set_thms = set_thms, |
329 set_selssss = set_selssss, |
331 set_selssss = set_selssss, |
330 set_introssss = set_introssss, |
332 set_introssss = set_introssss, |
331 set_cases = set_cases}, |
333 set_cases = set_cases}, |
332 fp_co_induct_sugar = |
334 fp_co_induct_sugar = |