src/HOL/Real/float_arith.ML
changeset 26803 0af0f674845d
parent 25300 bc3a1c964704