src/HOL/Real/real_arith.ML
changeset 23719 ccd9cb15c062
parent 23081 636cda81978a
child 24093 5d0ecd0c8f3c