src/HOL/Real.thy
changeset 58839 ccda99401bc8
parent 58789 387f65e69dd5
child 58834 773b378d9313