src/HOL/Tools/float_arith.ML
changeset 51213 7d08487aa603
parent 37391 476270a6c2dc
equal deleted inserted replaced
51212:2bbcc9cc12b4 51213:7d08487aa603