src/HOL/Real/RealDef.thy
changeset 17184 3d80209e9a53
parent 16973 b2a894562b8f
child 19023 5652a536b7e8