src/HOL/Quotient.thy
changeset 69008 d55783ea6cf6
parent 68616 cedf3480fdad
child 69605 a96320074298