src/HOL/Real/Rational.thy
changeset 24819 7d8e0a47392e
parent 24661 a705b9834590
child 25502 9200b36280c0