src/ZF/arith.thy
changeset 854 2e3ca37dfa14
parent 124 858ab9a9b047