src/HOL/Real/Rational.thy
changeset 20828 68ed2e514ca0
parent 20522 05072ae0d435
child 21404 eb85850d3eb7