src/HOL/Library/Quotient_Sum.thy
changeset 36348 89c54f51f55a
parent 35788 f1deaca15ca3
child 37678 0040bafffdef