src/HOL/Real.thy
changeset 75670 acf86c9f7698
parent 75543 1910054f8c39
child 75864 3842556b757c
equal deleted inserted replaced
75669:43f5dfb7fa35 75670:acf86c9f7698