src/HOL/Real/PNat.thy
changeset 13758 ee898d32de21
parent 12018 ec054019c910