src/HOL/NatArith.thy
changeset 20192 956cd30ef3be
parent 17688 91d3604ec4b5
child 21238 c46bc715bdfd