src/HOL/Algebra/abstract/RingHomo.thy
changeset 47639 2f7eb28c8b09
parent 35849 b5522b51cb1e