src/HOL/RealDef.thy
changeset 41478 18500bd1f47b
parent 41231 2e901158675e
child 41550 efa734d9b221