src/HOL/Real/RealDef.thy
changeset 22902 ac833b4bb7ee
parent 22456 6070e48ecb78
child 22958 b3a5569a81e5