src/HOL/Real/Real.ML
changeset 5325 f7a5e06adea1
parent 5184 9b8547a9496a
child 5459 1dbaf888f4e7
equal deleted inserted replaced
5324:ec84178243ff 5325:f7a5e06adea1