src/HOL/Real/RComplete.thy
changeset 10430 d3f780c3af0c
parent 9429 8ebc549e9326
child 14365 3d4df8c166ae
equal deleted inserted replaced
10429:8820f787e61e 10430:d3f780c3af0c