src/ZF/Sum.thy
changeset 58043 a90847f03ec8
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50