src/ZF/Arith.thy
changeset 8913 0bc13d5e60b8
parent 6070 032babd0120b
child 9491 1a36151ee2fc