src/HOL/Tools/float_arith.ML
changeset 39493 cb2208f2c07d
parent 37391 476270a6c2dc
equal deleted inserted replaced
39492:b1172d65dd28 39493:cb2208f2c07d