src/HOL/Real/real_arith.ML
changeset 18261 1318955d57ac
parent 17876 b9c92f384109
child 18708 4b3dadb4fe33
equal deleted inserted replaced
18260:5597cfcecd49 18261:1318955d57ac