src/HOL/Real/real_arith.ML
changeset 17851 2fa4f9b54761
parent 16827 c90a1f450327
child 17876 b9c92f384109