src/ZF/Sum.thy
changeset 49170 03bee3a6a1b7
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50