src/HOL/NatArith.thy
changeset 17391 c6338ed6caf8
parent 17085 5b57f995a179
child 17688 91d3604ec4b5