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