src/HOL/Rat.thy
changeset 39776 cde508d2eac8
parent 38857 97775f3e8722
child 39910 10097e0a9dbd
equal deleted inserted replaced
39775:e4c85d8c2aba 39776:cde508d2eac8