src/HOL/Real/rat_arith.ML
changeset 27353 71c4dd53d4cb
parent 27239 f2f42f9fa09d