src/ZF/arith.thy
changeset 8736 0bfd6678a5fa
parent 124 858ab9a9b047