src/HOL/Quotient.thy
changeset 70146 9839da71621f
parent 69990 eb072ce80f82
child 71262 a30278c8585f