src/HOL/Real/PNat.ML
changeset 9356 30c3d3e308ee
parent 9108 9fff97d29837
child 9422 4b6bc2b347e5