src/HOL/Fields.thy
changeset 69272 15e9ed5b28fb
parent 68547 549a4992222f
child 69502 0cf906072e20