equal
deleted
inserted
replaced
665 subsection {* ML setup *} |
665 subsection {* ML setup *} |
666 |
666 |
667 text {* Auxiliary data for the quotient package *} |
667 text {* Auxiliary data for the quotient package *} |
668 |
668 |
669 use "Tools/Quotient/quotient_info.ML" |
669 use "Tools/Quotient/quotient_info.ML" |
|
670 setup Quotient_Info.setup |
670 |
671 |
671 declare [[map "fun" = (map_fun, fun_rel)]] |
672 declare [[map "fun" = (map_fun, fun_rel)]] |
672 |
673 |
673 lemmas [quot_thm] = fun_quotient |
674 lemmas [quot_thm] = fun_quotient |
674 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp |
675 lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp |