src/HOL/Rational.thy
changeset 33003 1c93cfa807bc
parent 32657 5f13912245ff
child 33197 de6285ebcc05