src/ZF/Sum.thy
changeset 49614 0009a6ebc83b
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50