src/HOL/Library/Quotient_Sum.thy
changeset 36500 620f899158d4
parent 35788 f1deaca15ca3
child 37678 0040bafffdef