src/HOL/Archimedean_Field.thy
changeset 55307 59ab33f9d4de
parent 54489 03ff4d1e6784
child 58040 9a867afaab5a