src/HOL/Archimedean_Field.thy
changeset 78600 afb83ba8d24c
parent 77934 01c88cf514fc
child 78748 ca486ee0e4c5