src/HOL/Real/PNat.ML
changeset 14097 f4d2ff3cad09
parent 12842 32c9c881dec8