src/HOL/Real/RComplete.thy
changeset 12791 ccc0f45ad2c4
parent 9429 8ebc549e9326
child 14365 3d4df8c166ae
equal deleted inserted replaced
12790:8108791e2906 12791:ccc0f45ad2c4