src/HOL/Archimedean_Field.thy
changeset 62979 1e527c40ae40
parent 62623 dbc62f86a1a9
child 63331 247eac9758dd