src/ZF/Sum.thy
changeset 47544 e455cdaac479
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50