src/HOL/RealDef.thy
changeset 44262 355d5438f5fb
parent 43887 442aceb54969
child 44278 1220ecb81e8f