src/HOL/Real/RComplete.ML
changeset 5101 52e7c75acfe6
parent 5078 7b5ea59c0275
child 5143 b94cd208f073