src/HOL/Library/Quotient.thy
changeset 15705 b5edb9dcec9a
parent 15140 322485b816ac
child 18372 2bffdf62fe7f