src/HOL/Real/rat_arith.ML
changeset 25836 f7771e4f7064
parent 24196 f1dbfd7e3223
child 27154 026f3db3f5c6