src/HOL/Real.thy
changeset 64168 e573b985390c
parent 63961 2fd9656c4c82
child 64267 b9a1486e79be