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