src/ZF/Arith.thy
changeset 3872 a5839ecee7b8
parent 3840 e0baea4d485a
child 6070 032babd0120b