src/HOL/Real/PReal.thy
changeset 23719 ccd9cb15c062
parent 23389 aaca6a8e5414
child 24422 c0b5ff9e9e4d