HOL.Archimedean_Field