src/HOL/Library/Quotient_Product.thy
changeset 54947 9e632948ed56
parent 53012 cb82606b8215
child 55414 eab03e9cee8a