src/HOL/Tools/float_arith.ML
changeset 44341 a93d25fb14fc
parent 37391 476270a6c2dc
equal deleted inserted replaced
44340:3b859b573f1a 44341:a93d25fb14fc