src/HOL/Real/RComplete.thy
changeset 10689 5c44de6aadf4
parent 9429 8ebc549e9326
child 14365 3d4df8c166ae
equal deleted inserted replaced
10688:4cf4bbc25267 10689:5c44de6aadf4