src/HOL/Real.thy
changeset 64226 65f7d2eea2d7
parent 63961 2fd9656c4c82
child 64267 b9a1486e79be