src/HOL/NatArith.thy
changeset 17907 c20e4bddcb11
parent 17688 91d3604ec4b5
child 21238 c46bc715bdfd