src/HOL/Archimedean_Field.thy
changeset 79720 deb3056ed823
parent 78937 5e6b195eee83
child 79945 ca004ccf2352