src/HOL/NatDef.ML
changeset 9502 50ec59aff389
parent 9160 7a98dbf3e579
child 9870 2374ba026fc6