src/HOL/Real/rat_arith.ML
changeset 27090 2f45c1b1b05d
parent 24196 f1dbfd7e3223
child 27154 026f3db3f5c6