src/HOL/Tools/float_arith.ML
changeset 38475 1dd4f545ac24
parent 37391 476270a6c2dc
equal deleted inserted replaced
38474:e498dc2eb576 38475:1dd4f545ac24