src/HOL/NatArith.thy
changeset 14443 75910c7557c5
parent 14208 144f45277d5a
child 14607 099575a938e5