src/HOL/Hyperreal/hypreal_arith.ML
changeset 15234 ec91a90c604e
parent 15186 1fb9a1fe8d0c
child 15923 01d5d0c1c078