src/HOL/Real/rat_arith.ML
changeset 27885 76b51cd0a37c
parent 27239 f2f42f9fa09d