src/HOL/NatDef.ML
changeset 4537 4e835bd9fada
parent 4535 f24cebc299e4
child 4599 3a4348a3d6ff