src/HOL/Library/Quotient_Product.thy
changeset 38147 2b08a96a283e
parent 37678 0040bafffdef
child 39198 f967a16dfcdd