src/HOL/Nat.ML
changeset 9676 4a3c49420efd
parent 9637 47d39a31eb2f
child 9870 2374ba026fc6