src/HOL/NatDef.ML
changeset 13049 ce180e5b7fa0
parent 12841 c8ec6803d1cd