src/HOL/Real.thy
changeset 78646 fff610f1a6f4
parent 78250 400aecdfd71f
child 78669 18ea58bdcf77
equal deleted inserted replaced
78643:d5a1d64a563d 78646:fff610f1a6f4