src/HOL/Real/float_arith.ML
changeset 26766 0e2a29a1065c
parent 25300 bc3a1c964704