src/HOL/RealDef.thy
changeset 41249 26f12f98f50a
parent 41024 ba961a606c67
child 41231 2e901158675e