src/HOL/Archimedean_Field.thy
changeset 59863 30519ff3dffb
parent 59613 7103019278f0
child 59984 4f1eccec320c