src/HOL/Quotient.thy
changeset 36800 59b50c691b75
parent 36276 92011cc923f5
child 37049 ca1c293e521e