src/HOL/Archimedean_Field.thy
changeset 57354 ded92100ffd7
parent 54489 03ff4d1e6784
child 58040 9a867afaab5a