src/HOL/Archimedean_Field.thy
changeset 78564 8ba186dc9bc8
parent 77934 01c88cf514fc
child 78748 ca486ee0e4c5