2537 |
2537 |
2538 val fp_res = |
2538 val fp_res = |
2539 {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs, |
2539 {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs, |
2540 xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, |
2540 xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, |
2541 ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, |
2541 ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, |
2542 xtor_maps = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss', |
2542 xtor_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss', |
2543 xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, |
2543 xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms, |
2544 xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm, |
2544 xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm, |
2545 dtor_set_inducts = dtor_Jset_induct_thms, |
2545 dtor_set_inducts = dtor_Jset_induct_thms, |
2546 xtor_co_rec_transfers = dtor_corec_transfer_thms}; |
2546 xtor_co_rec_transfers = dtor_corec_transfer_thms}; |
2547 in |
2547 in |