src/HOL/Real/rat_arith.ML
changeset 20326 cbf31171c147
parent 20254 58b71535ed00
child 21243 afffe1f72143