src/HOL/Quotient.thy
changeset 81351 95cb584cb777
parent 81128 5b201b24d99b