src/ZF/Arith.thy
changeset 4707 abe6f28a38c1
parent 3840 e0baea4d485a
child 6070 032babd0120b