src/HOL/NatDef.ML
changeset 12378 86c58273f8c0
parent 11868 56db9f3a6b3e
child 12841 c8ec6803d1cd