src/HOL/Fields.thy
changeset 78130 8234c42d20e6
parent 75880 714fad33252e
child 79541 4f40225936d1