src/HOL/NatDef.ML
changeset 13447 3470596f3cd5
parent 12841 c8ec6803d1cd