src/HOL/Real/RComplete.thy
changeset 16377 9da1cf997e79
parent 15539 333a88244569
child 16819 00d8f9300d13