src/HOL/Hyperreal/HyperArith0.ML
changeset 11718 92706a69dacc
parent 11704 3c50a2cd6f00
child 12018 ec054019c910