src/HOL/NatDef.ML
changeset 9346 297dcbf64526
parent 9160 7a98dbf3e579
child 9870 2374ba026fc6