src/HOL/Real.thy
changeset 75841 7c00d5266bf8
parent 75543 1910054f8c39
child 75864 3842556b757c