src/ZF/sum.thy
changeset 11982 65e2822d83dd
parent 124 858ab9a9b047