src/HOL/Archimedean_Field.thy
changeset 79755 3066125a7f51
parent 78937 5e6b195eee83
child 79945 ca004ccf2352