src/ZF/Arith.thy
changeset 9230 17ae63f82ad8
parent 6070 032babd0120b
child 9491 1a36151ee2fc