src/HOL/Real/PRat.thy
changeset 14097 f4d2ff3cad09
parent 13487 1291c6375c29