src/HOL/Real/PReal.thy
changeset 23563 42f2f90b51a6
parent 23389 aaca6a8e5414
child 24422 c0b5ff9e9e4d