src/HOL/Library/Quotient_Product.thy
changeset 50411 c9023d78d1a6
parent 47982 7aa35601ff65
child 51377 7da251a6c16e