src/HOL/Library/Quotient_Product.thy
changeset 55400 1e8dd9cd320b
parent 53012 cb82606b8215
child 55414 eab03e9cee8a