src/ZF/arith.thy
changeset 263 d45f0af592f0
parent 124 858ab9a9b047