equal
deleted
inserted
replaced
293 |
293 |
294 print_quotients |
294 print_quotients |
295 |
295 |
296 ML {* val qty = @{typ "'a fset"} *} |
296 ML {* val qty = @{typ "'a fset"} *} |
297 ML {* val rsp_thms = |
297 ML {* val rsp_thms = |
298 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
298 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
299 @ @{thms ho_all_prs ho_ex_prs} *} |
|
300 |
299 |
301 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
300 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
302 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
301 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
303 ML {* val consts = lookup_quot_consts defs *} |
302 ML {* val consts = lookup_quot_consts defs *} |
304 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
303 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |