src/HOL/Quotient.thy
changeset 55430 8eb6c740ec1a
parent 54867 c21a2465cac1
child 55945 e96383acecf9