src/HOL/Real/float_arith.ML
changeset 27090 2f45c1b1b05d
parent 25300 bc3a1c964704