src/HOL/NatDef.thy
changeset 12566 fe20540bcf93
parent 12338 de0f4a63baa5