src/ZF/arith.thy
changeset 4365 fbb275398eb7
parent 124 858ab9a9b047