src/HOL/Archimedean_Field.thy
changeset 77830 0f2baf04b782
parent 77490 2c86ea8961b5
child 77934 01c88cf514fc