src/HOL/Real.thy
changeset 75168 ff60b4acd6dd
parent 73932 fd21b4a93043
child 75327 f4a39342111b
equal deleted inserted replaced
75167:0a300751fdf5 75168:ff60b4acd6dd