src/HOL/Hyperreal/hypreal_arith.ML
changeset 17713 7efbe0ec9d4c
parent 17431 70311ad8bf11
child 17876 b9c92f384109