src/HOL/RealDef.thy
changeset 41719 91c2510e19c5
parent 41550 efa734d9b221
child 41792 ff3cb0c418b7