src/HOL/Hyperreal/hypreal_arith.ML
changeset 20830 65ba80cae6df
parent 20254 58b71535ed00
child 24075 366d4d234814