src/HOL/NatDef.thy
changeset 11371 1d5d181b7e28
parent 11326 680ebd093cfe
child 11464 ddea204de5bc