src/HOL/NatDef.thy
changeset 13066 b57d926d1de2
parent 12338 de0f4a63baa5