src/HOL/Real/RealOrd.ML
changeset 9502 50ec59aff389
parent 9434 d2fa043ab24f
child 9825 a0fcf6f0436c