src/HOL/NatDef.ML
changeset 10168 50be659d4222
parent 9969 4753185f1dd2
child 10186 499637e8f2c6