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