src/HOL/NatArith.thy
changeset 15572 9c89b1adf573
parent 15539 333a88244569
child 15861 cf2c6cf35216