src/HOL/Real/PReal.ML
changeset 13462 56610e2ba220
parent 13438 527811f00c56
child 13601 fd3e3d6b37b2