src/HOL/Tools/float_arith.ML
changeset 47607 5c17ef8feac7
parent 37391 476270a6c2dc
equal deleted inserted replaced
47606:06dde48a1503 47607:5c17ef8feac7