src/ZF/Sum.thy
changeset 76954 52f3d1cd8d63
parent 76216 9fc34f76b4e8