src/HOL/NatArith.thy
changeset 14502 0c135fa75626
parent 14208 144f45277d5a
child 14607 099575a938e5