src/HOL/Tools/float_arith.ML
changeset 29339 d8df32ab1172
parent 28952 15a4b2cf8c34
child 29804 e15b74577368
equal deleted inserted replaced
29331:dfaf9d086868 29339:d8df32ab1172