src/HOL/Real/real_arith.ML
changeset 14360 e654599b114e
parent 14356 9e3ce012f843
child 14365 3d4df8c166ae