src/HOL/Tools/float_arith.ML
changeset 37460 910b2422571d
parent 37391 476270a6c2dc
equal deleted inserted replaced
37459:7a3610dca96b 37460:910b2422571d