src/HOL/Real/RealDef.thy
changeset 7165 8c937127fd8c
parent 7127 48e235179ffb
child 7219 4e3f386c2e37