src/HOL/Real/RealDef.thy
changeset 14360 e654599b114e
parent 14348 744c868ee0b7
child 14365 3d4df8c166ae