src/HOL/NatDef.ML
changeset 9143 6180c29d2db6
parent 9108 9fff97d29837
child 9160 7a98dbf3e579