src/HOL/Library/Quotient_Sum.thy
changeset 36357 641a521bfc19
parent 35788 f1deaca15ca3
child 37678 0040bafffdef