src/HOL/Real/PNat.ML
changeset 9502 50ec59aff389
parent 9422 4b6bc2b347e5
child 9635 c9ebf0a1d712