src/HOL/Hyperreal/HyperBin.ML
changeset 12130 30d9143aff7e
parent 12018 ec054019c910
child 13462 56610e2ba220