src/HOL/RealDef.thy
changeset 38286 c9c7bd836894
parent 38242 f26d590dce0f
child 38287 796302ca3611