src/HOL/NatDef.ML
changeset 6554 5be3f13193d7
parent 6115 c70bce7deb0f
child 7030 53934985426a