src/HOL/Quotient.thy
changeset 71297 9f2085c499a2
parent 71262 a30278c8585f
child 71354 c71a44893645