src/HOL/Real/real_arith.ML
changeset 23586 7d6b1d800dc4
parent 23081 636cda81978a
child 24093 5d0ecd0c8f3c