src/HOL/Real/RealOrd.ML
changeset 11565 ab004c0ecc63
parent 11464 ddea204de5bc
child 11599 12cc28aafb4d
equal deleted inserted replaced
11564:7b87c95fdf3b 11565:ab004c0ecc63