src/HOL/NatDef.ML
changeset 9685 6d123a7e30bd
parent 9160 7a98dbf3e579
child 9870 2374ba026fc6