src/HOL/Quotient.thy
changeset 70113 c8deb8ba6d05
parent 69990 eb072ce80f82
child 71262 a30278c8585f