src/HOL/Arith.thy
changeset 7596 c97c3ad15d2e
parent 5183 89f162de39cf
child 8929 4829556a56f8