src/HOL/Real/RealDef.thy
changeset 28263 69eaa97e7e96
parent 28091 50f2d6ba024c
child 28351 abfc66969d1f