src/HOL/RealDef.thy
changeset 41219 41f3fdc49ec3
parent 41024 ba961a606c67
child 41231 2e901158675e