src/HOL/Real.thy
changeset 65202 187277b77d50
parent 64267 b9a1486e79be
child 65885 77d922eff5ac
equal deleted inserted replaced
65201:2d01b30e6ac6 65202:187277b77d50