src/HOL/Library/Quotient_Product.thy
changeset 47884 21c42b095c84
parent 47777 f29e7dcd7c40
child 47936 756f30eac792