src/ZF/sum.thy
changeset 3861 834ed1471732
parent 124 858ab9a9b047