src/HOL/Real/rat_arith.ML
changeset 15341 254f6f00b60e
parent 15186 1fb9a1fe8d0c
child 15923 01d5d0c1c078