src/HOL/Algebra/Finite_Extensions.thy
changeset 81776 c6d8db03dfdc
parent 73655 26a1d66b9077