src/HOL/Archimedean_Field.thy
changeset 76376 934d4aed8497
parent 75878 fcd118d9242f
child 77490 2c86ea8961b5