src/HOL/Real/RealDef.thy
changeset 18777 9d98d5705433
parent 16973 b2a894562b8f
child 19023 5652a536b7e8