src/HOL/RealDef.thy
changeset 41670 74010c6af0a4
parent 41550 efa734d9b221
child 41792 ff3cb0c418b7