src/HOL/Archimedean_Field.thy
changeset 78684 aa532cf1c894
parent 77934 01c88cf514fc
child 78748 ca486ee0e4c5