src/HOL/Hyperreal/hypreal_arith.ML
changeset 26402 441ddf3b8f02
parent 24093 5d0ecd0c8f3c