src/HOL/Quotient.thy
changeset 54784 54f1ce13c140
parent 54555 e8c5e95d338b
child 54867 c21a2465cac1