src/HOL/Rat.thy
changeset 78130 8234c42d20e6
parent 77179 6d2ca97a8f46
child 80061 4c1347e172b1
equal deleted inserted replaced
78129:acf27e8352d2 78130:8234c42d20e6