src/HOL/RealDef.thy
changeset 45140 339a8b3c4791
parent 45051 c478d1876371
child 45184 426dbd896c9e