src/ZF/Sum.thy
changeset 80398 4953d52e04d2
parent 76216 9fc34f76b4e8