src/HOL/Real/PReal.thy
changeset 15216 2fac1f11b7f6
parent 15140 322485b816ac
child 15234 ec91a90c604e