src/HOL/Library/Quotient.thy
changeset 13049 ce180e5b7fa0
parent 12371 80ca9058db95
child 14706 71590b7733b7