src/HOL/Nat.ML
changeset 9697 c5fc121c2067
parent 9637 47d39a31eb2f
child 9870 2374ba026fc6