src/HOL/Real.thy
changeset 75653 ea4f5b0ef497
parent 75543 1910054f8c39
child 75864 3842556b757c