src/HOL/Real/PReal.thy
changeset 18396 b3e7da94b51f
parent 18215 a28879118978
child 18429 42ee9f24f63a