src/HOL/Real/rat_arith.ML
changeset 23830 f838adde842d
parent 23346 1517207ec8b9
child 24093 5d0ecd0c8f3c