src/HOL/Real/PReal.ML
changeset 10618 5b96bc5fbec3
parent 10292 19753287b9df
child 10752 c4f1bf2acf4c