src/HOL/NatDef.ML
changeset 12655 b8c130dc46be
parent 11868 56db9f3a6b3e
child 12841 c8ec6803d1cd