src/HOL/Library/Quotient_Sum.thy
changeset 36964 a354605f03dc
parent 35788 f1deaca15ca3
child 37678 0040bafffdef