src/HOL/Real/RealDef.thy
changeset 19088 7870cf61c4b3
parent 19023 5652a536b7e8
child 19765 dfe940911617