src/HOL/Real/Rational.thy
changeset 27090 2f45c1b1b05d
parent 26732 6ea9de67e576
child 27509 63161d5f8f29