src/ZF/Sum.thy
changeset 80408 e6d3d1db6136
parent 76216 9fc34f76b4e8