src/ZF/sum.thy
changeset 13332 f130bcf29620
parent 124 858ab9a9b047