src/HOL/NatDef.thy
changeset 13117 0b233f430076
parent 12338 de0f4a63baa5