src/HOL/Hyperreal/hypreal_arith.ML
changeset 17713 7efbe0ec9d4c
parent 17431 70311ad8bf11
child 17876 b9c92f384109
equal deleted inserted replaced
17712:46c2091e5187 17713:7efbe0ec9d4c