src/HOL/NatDef.ML
changeset 13117 0b233f430076
parent 12841 c8ec6803d1cd