src/HOL/NatArith.thy
changeset 14872 3f2144aebd76
parent 14607 099575a938e5
child 14981 e73f8140af78