src/HOL/Hyperreal/hypreal_arith.ML
changeset 22422 ee19cdb07528
parent 20254 58b71535ed00
child 24075 366d4d234814