src/HOL/Quotient.thy
changeset 57514 bdc2c6b40bf2
parent 56073 29e308b56d23
child 57960 ee1ba4848896