src/HOL/Hyperreal/hypreal_arith.ML
changeset 17740 fc385ce6187d
parent 17431 70311ad8bf11
child 17876 b9c92f384109