src/HOL/NatDef.ML
changeset 12050 6934c005aec4
parent 11868 56db9f3a6b3e
child 12841 c8ec6803d1cd