src/HOL/Hyperreal/hypreal_arith.ML
changeset 21471 03a5ef1936c5
parent 20254 58b71535ed00
child 24075 366d4d234814