src/HOL/RealDef.thy
changeset 35437 fe196f61b970
parent 35344 e0b46cd72414
child 35635 90fffd5ff996