src/HOL/Quotient.thy
changeset 81954 6f2bcdfa9a19
parent 81128 5b201b24d99b