src/HOL/Real/Real.ML
changeset 5526 e7617b57a3e6
parent 5521 7970832271cc
child 5535 678999604ee9