equal
deleted
inserted
replaced
747 subsection {* ML setup *} |
747 subsection {* ML setup *} |
748 |
748 |
749 text {* Auxiliary data for the quotient package *} |
749 text {* Auxiliary data for the quotient package *} |
750 |
750 |
751 named_theorems quot_equiv "equivalence relation theorems" |
751 named_theorems quot_equiv "equivalence relation theorems" |
752 named_theorems quot_respect "respectfulness theorems" |
752 and quot_respect "respectfulness theorems" |
753 named_theorems quot_preserve "preservation theorems" |
753 and quot_preserve "preservation theorems" |
754 named_theorems id_simps "identity simp rules for maps" |
754 and id_simps "identity simp rules for maps" |
755 named_theorems quot_thm "quotient theorems" |
755 and quot_thm "quotient theorems" |
756 ML_file "Tools/Quotient/quotient_info.ML" |
756 ML_file "Tools/Quotient/quotient_info.ML" |
757 |
757 |
758 declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]] |
758 declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]] |
759 |
759 |
760 lemmas [quot_thm] = fun_quotient3 |
760 lemmas [quot_thm] = fun_quotient3 |