src/HOL/NatDef.ML
changeset 9803 bc883b390d91
parent 9160 7a98dbf3e579
child 9870 2374ba026fc6