src/HOL/Archimedean_Field.thy
changeset 82734 89347c0cc6a3
parent 82689 817f97d8cd26