src/HOL/NatDef.ML
changeset 9481 b16624f1ea38
parent 9160 7a98dbf3e579
child 9870 2374ba026fc6