src/HOL/Hyperreal/HyperOrd.ML
changeset 11170 015af2fc7026
parent 10919 144ede948e58
child 11701 3d51fbf81c17