src/HOL/Real/RealDef.thy
changeset 10841 2fb8089ab6cd
parent 10834 a7897aebbffc
child 10919 144ede948e58