src/HOL/Rat.thy
changeset 81776 c6d8db03dfdc
parent 81124 6ce0c8d59f5a
child 82310 41f5266e5595