src/HOL/Archimedean_Field.thy
changeset 77683 3e8e749935fc
parent 77490 2c86ea8961b5
child 77934 01c88cf514fc