src/HOL/Real/RComplete.thy
changeset 16633 208ebc9311f2
parent 15539 333a88244569
child 16819 00d8f9300d13
equal deleted inserted replaced
16632:ad2895beef79 16633:208ebc9311f2