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