src/HOL/Real/float.ML
changeset 21966 edab0ecfbd7c
parent 21820 2f2b6a965ccc
child 22578 b0eb5652f210