src/HOL/Real/PNat.ML
changeset 5139 013ea0f023e3
parent 5078 7b5ea59c0275
child 5143 b94cd208f073