src/HOL/Real.thy
changeset 75841 7c00d5266bf8
parent 75543 1910054f8c39
child 75864 3842556b757c
equal deleted inserted replaced
75840:f8c412a45af8 75841:7c00d5266bf8