293 |
293 |
294 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec |
294 fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec |
295 co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
295 co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss |
296 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...}, |
296 ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...}, |
297 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
297 fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, |
298 rel_intros, rel_cases, set_thms, set_selssss, set_intros, set_cases, ...}, |
298 rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
299 fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
300 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, |
301 ...} : fp_sugar) = |
301 ...} : fp_sugar) = |
302 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
302 {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, |
303 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
303 pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, |
318 rel_sels = rel_sels, |
318 rel_sels = rel_sels, |
319 rel_intros = rel_intros, |
319 rel_intros = rel_intros, |
320 rel_cases = rel_cases, |
320 rel_cases = rel_cases, |
321 set_thms = set_thms, |
321 set_thms = set_thms, |
322 set_selssss = set_selssss, |
322 set_selssss = set_selssss, |
323 set_intros = set_intros, |
323 set_introssss = set_introssss, |
324 set_cases = set_cases}, |
324 set_cases = set_cases}, |
325 fp_co_induct_sugar = |
325 fp_co_induct_sugar = |
326 {co_rec = co_rec, |
326 {co_rec = co_rec, |
327 common_co_inducts = common_co_inducts, |
327 common_co_inducts = common_co_inducts, |
328 co_inducts = co_inducts, |
328 co_inducts = co_inducts, |