src/HOL/Real/float_arith.ML
changeset 26877 c3bb1f397811
parent 25300 bc3a1c964704