src/HOL/Real/PRat.ML
changeset 12990 c11adf2b1c1e
parent 12018 ec054019c910
child 13438 527811f00c56
equal deleted inserted replaced
12989:42ac77552dbf 12990:c11adf2b1c1e