src/HOL/Real.thy
changeset 76521 15f868460de9
parent 75864 3842556b757c
child 77490 2c86ea8961b5
equal deleted inserted replaced
76519:137cec33346f 76521:15f868460de9