src/HOL/Nat.ML
changeset 3718 d78cf498a88c
parent 3023 01364e2f30ad
child 4686 74a12e86b20b