src/HOL/RealDef.thy
changeset 43855 01b13e9a1a7e
parent 43733 a6ca7b83612f
child 43887 442aceb54969