src/ZF/Arith.thy
changeset 3229 cb3c27f2753e
parent 2469 b50b8c0eec01
child 3840 e0baea4d485a