src/HOL/Real/real_arith.ML
changeset 23563 42f2f90b51a6
parent 23081 636cda81978a
child 24093 5d0ecd0c8f3c