src/HOL/Quotient.thy
changeset 70490 c42a0a0a9a8d
parent 69990 eb072ce80f82
child 71262 a30278c8585f