src/HOL/Real/float.ML
changeset 21125 9b7d35ca1eef
parent 20767 9bc632ae588f
child 21820 2f2b6a965ccc