src/HOL/Archimedean_Field.thy
changeset 78761 6b3f13d39612
parent 77934 01c88cf514fc
child 78748 ca486ee0e4c5