src/ZF/nat.thy
changeset 9147 9a64807da023
parent 124 858ab9a9b047