src/HOL/Real/float_arith.ML
changeset 25655 e55626a33a8e
parent 25300 bc3a1c964704