src/HOL/Archimedean_Field.thy
changeset 79800 abb5e57c92a7
parent 78937 5e6b195eee83
child 79945 ca004ccf2352