src/HOL/NatDef.ML
changeset 6477 e36581d04eee
parent 6115 c70bce7deb0f
child 7030 53934985426a