src/HOL/Real/PRat.thy
changeset 9356 30c3d3e308ee
parent 8856 435187ffc64e
child 9391 a6ab3a442da6