src/HOL/Real/PReal.thy
changeset 19720 f68f6f958a1d
parent 18433 51a99fff78b2
child 19765 dfe940911617
equal deleted inserted replaced
19719:837025cc6317 19720:f68f6f958a1d