src/HOL/Quotient.thy
changeset 46368 ded0390eceae
parent 45961 5cefe17916a6
child 46468 4db76d47b51a