src/HOL/Quotient.thy
changeset 38350 480b2de9927c
parent 38317 cb8e2ac6397b
child 38702 72fd257f4343