src/HOL/Quotient.thy
changeset 81810 6cd42e67c0a8
parent 81128 5b201b24d99b