src/HOL/Nat.ML
changeset 8450 dc44d6533f0f
parent 8442 96023903c2df
child 8942 6aad5381ba83