src/HOL/Library/Quotient.thy
changeset 17643 7e417a7cbf9f
parent 15140 322485b816ac
child 18372 2bffdf62fe7f