src/HOL/Nat.ML
changeset 15916 1314ef1e49dd
parent 15413 901d1bfedf09
child 15921 b6e345548913