src/HOL/Real/real_arith.ML
changeset 22237 bb9b1c8a8a95
parent 20254 58b71535ed00
child 22962 4bb05ba38939
equal deleted inserted replaced
22236:1502e0138d5b 22237:bb9b1c8a8a95