src/HOL/Hyperreal/hypreal_arith0.ML
changeset 11804 d69e7acd9380
parent 11704 3c50a2cd6f00
child 12018 ec054019c910