src/HOL/Nat.ML
changeset 17907 c20e4bddcb11
parent 17274 746bb4c56800
child 21669 c68717c16013