src/HOL/Hyperreal/hypreal_arith.ML
changeset 19499 1a082c1257d7
parent 18708 4b3dadb4fe33
child 20254 58b71535ed00
equal deleted inserted replaced
19498:7dcf9903eeb3 19499:1a082c1257d7