src/HOL/Quotient.thy
changeset 55797 6a59b4bb7506
parent 54867 c21a2465cac1
child 55945 e96383acecf9