src/HOL/Archimedean_Field.thy
changeset 78224 d85d0d41b2bd
parent 77934 01c88cf514fc
child 78748 ca486ee0e4c5