src/HOL/Real/RComplete.ML
changeset 5526 e7617b57a3e6
parent 5521 7970832271cc
child 5588 a3ab526bb891