src/HOL/NatArith.thy
changeset 14600 ba51bc239716
parent 14208 144f45277d5a
child 14607 099575a938e5