src/HOL/Real/real_arith.ML
changeset 10618 5b96bc5fbec3
parent 10574 8f98f0301d67
child 10693 9e4a0e84d0d6