src/HOL/Library/Quotient_Product.thy
changeset 35536 1f980bbc6ad8
parent 35222 4f1fba00f66d
child 35788 f1deaca15ca3