src/HOL/Archimedean_Field.thy
changeset 45504 cad35ed6effa
parent 43733 a6ca7b83612f
child 47108 2a1953f0d20d