src/HOL/Hyperreal/hypreal_arith.ML
changeset 20849 389cd9c8cfe1
parent 20254 58b71535ed00
child 24075 366d4d234814
equal deleted inserted replaced
20848:27a09c3eca1f 20849:389cd9c8cfe1