src/HOL/Real/RComplete.ML
changeset 5253 82a5ca6290aa
parent 5143 b94cd208f073
child 5521 7970832271cc