src/HOL/Quotient.thy
changeset 55370 e6be866b5f5b
parent 54867 c21a2465cac1
child 55945 e96383acecf9