src/HOL/Real.thy
changeset 56650 1f9ab71d43a5
parent 56571 f4635657d66f
child 56889 48a745e1bde7
equal deleted inserted replaced
56649:16e1fa9d094f 56650:1f9ab71d43a5