src/HOL/Real/PRat.ML
changeset 7711 4dae7a4fceaf
parent 7376 46f92a120af9
child 7825 1be9b63e7d93
equal deleted inserted replaced
7710:bf8cb3fc5d64 7711:4dae7a4fceaf