src/HOL/Library/Quotient.thy
changeset 13413 0b60b9e18a26
parent 12371 80ca9058db95
child 14706 71590b7733b7