src/HOL/Quotient.thy
changeset 69022 e2858770997a
parent 68616 cedf3480fdad
child 69605 a96320074298